| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey |
| 2014-01-05 | Proof_using: new syntax + suggestion | Enrico Tassi |
| 2013-11-02 | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | aspiwack |
| 2013-02-17 | Revised the Ltac trace mechanism so that trace breaking due to | herbelin |
| 2012-07-11 | Severe reorganisation of the code of tactics in Proofview. | aspiwack |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-03-20 | Many changes in the Makefile infrastructure + a beginning of ocamlbuild | letouzey |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |