SkillAgentSearch skills...

Paramcoq

Old Coq plugin for parametricity [maintainer=@ppedrot]

Install / Use

/learn @rocq-community/Paramcoq
About this skill

Quality Score

0/100

Supported Platforms

Universal

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.

View on GitHub
GitHub Stars44
CategoryDevelopment
Updated2h ago
Forks29

Languages

OCaml

Security Score

80/100

Audited on Mar 31, 2026

No findings