rocq-community/paramcoq

Old Coq plugin for parametricity [maintainer=@ppedrot]

OCaml

44

392 commits

updated Aug 20, 2026

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.

coq

coq-ci

coq-platform

coq-plugin

docker-coq-action

parametricity

Contributors

89 commits

79 commits

65 commits

44 commits

Similar repos

coq-community/paramcoq

Old Coq plugin for parametricity [maintainer=@ppedrot]

44

rocq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources…

395

rocq-community/docker-coq

Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-act…

40

rocq-community/coq-dpdgraph

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

101

rocq-community/parseque

Total Parser Combinators in Coq [maintainer=@womeier]

51

rocq-community/manifesto

Documentation on goals of the Rocq-community organization, the shared contributing guide and code…

75

rocq-community/coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

135

snu-sf/paco

A Coq library for parametric coinduction

55

Languages

OCaml

48.7%

Rocq Prover

48.0%

Python

1.7%

rocq-community/paramcoq

Old Coq plugin for parametricity [maintainer=@ppedrot]

OCaml

44

392 commits

updated Aug 20, 2026

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.

coq

coq-ci

coq-platform

coq-plugin

docker-coq-action

parametricity

Similar repos

coq-community/paramcoq

Old Coq plugin for parametricity [maintainer=@ppedrot]

44

rocq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources…

395

rocq-community/docker-coq

Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-act…

40

rocq-community/coq-dpdgraph

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

101

rocq-community/parseque

Total Parser Combinators in Coq [maintainer=@womeier]

51

rocq-community/manifesto

Documentation on goals of the Rocq-community organization, the shared contributing guide and code…

75

rocq-community/coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

135

snu-sf/paco

A Coq library for parametric coinduction

55

Contributors

89 commits

79 commits

65 commits

44 commits

Languages

OCaml

48.7%

Rocq Prover

48.0%

Python

1.7%