Yves Bertot

plugin_tutorials. A collection of small projects to illustrate how to write plugins for Coq

HoTT. Homotopy type theory

opam-coq-archive. Archive for all Coq related OPAM packages organized in various repositories

norm_union_example. A experience to describe the termination of difficult function, question from stackexchange

pi-agm. A formal description in Coq of computations of PI using arithmetic-geometric means

breadth_first_search. A generic algorithm for breadth first search, in Coq, with proofs

fset_exercises. Didactic material for Coq

coind_filters. Coq code associated to an article published at TLCA'05 "Filters on Co-inductive Streams..."

coq-dpdgraph. Build dependency graphs between COQ objects

one_num_type. Rocq Prover