aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview_monad.mli
Commit message (Expand)AuthorAge
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
* Adding a tail-rec tclONCE.Gravatar Pierre-Marie Pédrot2014-07-24
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Adding a [map] primitive to the tactic monad. Hopefully this should beGravatar Pierre-Marie Pédrot2014-04-20
* Transfering the initial goals from the proofview to the proof object.Gravatar Pierre-Marie Pédrot2014-04-07
* Adding an [modify] function to the tactic monad. It allows to modifyGravatar Pierre-Marie Pédrot2014-04-06
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* A dedicated view type for Proofview_gen.split.Gravatar aspiwack2013-11-02
* Makes the Ltac debugger usable again.Gravatar aspiwack2013-11-02
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...Gravatar aspiwack2013-11-02