Incorrect parameter declaration in Rocq output

[simonr89]

Description of the issue

The type declaration for function symbols is not correct in the Rocq output, and consequently doesn't typecheck. For example a unary predicate f is declared as

Parameter f : (goeland_U > Prop).

instead of

Parameter f : (goeland_U -> Prop).

Flags used

-orocq

Small problem file to reproduce the bug

No response

Version of Goéland where the issue occurs

v.1.2-dev.r40732d6cca0f37bb553896779d645720d06209a7

[jrosain]

Duplicate of #52.

Should be fixed once #59 is merged.

[jrosain]

If you urgently need the Rocq output, I think it's safe to use the branch jrosain:fix-rocq-output, it should have all the latest bug fixes.

Beware that the Lambdapi output is probably broken since since v1.1, which has other serious problems. I'll whip up a branch that fixes the Lambdapi output soon (if possible, I'll try to have it ready for next week, but no promises here).

I'm closing this issue as duplicate.