aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview_monad.mli
Commit message (Expand)AuthorAge
* Moving Proofview_monad to the engine/ folder.Gravatar Pierre-Marie Pédrot2015-02-28
* Update headers.Gravatar Maxime Dénès2015-01-12
* Info: do not record info trace unless needed.Gravatar Arnaud Spiwack2014-11-01
* An API for info traces.Gravatar Arnaud Spiwack2014-11-01
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a [make] primitive to the NonLogical monad.Gravatar Pierre-Marie Pédrot2014-08-05
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
* Some comments in the interface of Proofview_monad.Gravatar Arnaud Spiwack2014-08-04
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
* 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