Old Coq plugin for parametricity [maintainer=@ppedrot]
44
stars
392
commits
OCaml
primary language
Aug 20, 2026
updated
README
Deprecation Notice
Paramcoq is no longer actually maintained and released. It is only kept as a test case for Rocq's OCaml API. The release for Rocq 9.0 will be the last one and is known to suffer some universe issues (for instance iit no longer enable to compile CoqEAL). Users are invited to switch to coq-elpi derive.param2. One can look at CoqEAL for an example of porting. Main current caveat: support for mutual inductives isn't implemented yet.
See old README for previous documentation.
Contributors
Similar repos
Languages
OCaml
48.7%
Rocq Prover
48.0%
Python
1.7%
Old Coq plugin for parametricity [maintainer=@ppedrot]
44
stars
392
commits
OCaml
primary language
Aug 20, 2026
updated
README
Deprecation Notice
Paramcoq is no longer actually maintained and released. It is only kept as a test case for Rocq's OCaml API. The release for Rocq 9.0 will be the last one and is known to suffer some universe issues (for instance iit no longer enable to compile CoqEAL). Users are invited to switch to coq-elpi derive.param2. One can look at CoqEAL for an example of porting. Main current caveat: support for mutual inductives isn't implemented yet.
See old README for previous documentation.
Similar repos
Contributors
Languages
OCaml
48.7%
Rocq Prover
48.0%
Python
1.7%