coq-plugin topic
PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
pumpkin-pi
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
ltac2
A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository.
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
atbr
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
paramcoq
Coq plugin for parametricity [maintainer=@proux01]
coq-plugin-template
Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]
coq-tactician
A Seamless, Interactive Tactic Learner and Prover for Coq
metaprogramming-rosetta-stone
A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]