| Age | Commit message (Expand) | Author |
|---|---|---|
| 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 |