| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-10-27 | Make sure that Logic/ExtensionalityFacts gets compiled. | Guillaume Melquiond |
| 2014-07-15 | Added a (constructive) proof of Weak Konig's lemma for decidable trees. | Hugo Herbelin |
| 2014-06-26 | Remove some theories that have been deprecated for 10 years. | Guillaume Melquiond |
| 2014-02-07 | FinFun.v: results about injective/surjective/bijective fonctions over finite ... | Pierre Letouzey |
| 2013-06-02 | A constructive proof of Fan theorem where paths are represented by predicates. | herbelin |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |