| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-02-16 | Removing non-marshallable data from the Agram constructor. Instead of | Pierre-Marie Pédrot |
| 2014-01-14 | Removing unused tactics in rewrite. | Pierre-Marie Pédrot |
| 2013-12-04 | Vernac classification: allow for commands which start proofs but must be sync... | Arnaud Spiwack |
| 2013-11-02 | The tactic [admit] exits with the "unsafe" status. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-09-26 | Opacifying the type of strategies. | ppedrot |
| 2013-09-26 | Splitting Rewrite into a code part and a CAMLP4-dependent one. | ppedrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |