Coq plugin for parametricity [maintainer=@proux01]

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

A Seamless, Interactive Tactic Learner and Prover for Coq

A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository.

Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]

Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]

Library of useful utility functions for Coq plugins

Fixpoint to eliminator translation in Coq

Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

A Coq plugin for Codewars

Useful utility functions for writing Coq plugins

Coq plugin for plain dependency extraction

REPLICA: REPL Instrumentation for Coq Analysis

Build dependency graphs between COQ objects

Coq plugin for printing term abstract syntax trees and their digests