| Age | Commit message (Expand) | Author |
|---|---|---|
| 2013-11-02 | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | aspiwack |
| 2013-11-02 | The tactic [admit] exits with the "unsafe" status. | aspiwack |
| 2013-11-02 | Cleanup of comments. | aspiwack |
| 2013-11-02 | Small change to the IO monad interface: [val ref : 'a -> 'a ref t] | aspiwack |
| 2013-11-02 | Bases tactics on an IO monad. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-01-28 | Added backtrace information to anomalies | ppedrot |
| 2012-07-11 | Severe reorganisation of the code of tactics in Proofview. | aspiwack |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |