coq - The formal proof system

Age	Commit message (Expand)	Author
2015-02-28	Moving Proofview_monad to the engine/ folder.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-11-01	Info: do not record info trace unless needed.	Arnaud Spiwack
2014-11-01	An API for info traces.	Arnaud Spiwack
2014-10-22	Split [Proofview] into a file where the basic operations on the state are def...	Arnaud Spiwack
2014-10-22	Make names in [Proofview_monad] more uniform.	Arnaud Spiwack
2014-10-16	Refactoring proofview: make the definition of the logic monad polymorphic.	Arnaud Spiwack
2014-09-04	Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.	Pierre-Marie Pédrot
2014-09-04	Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."	Pierre-Marie Pédrot
2014-08-05	Adding a [make] primitive to the NonLogical monad.	Pierre-Marie Pédrot
2014-08-05	Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].	Arnaud Spiwack
2014-08-04	Cleaning the new implementation of the tactic monad continued.	Arnaud Spiwack
2014-05-06	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau
2014-05-06	Rewriting the proof monad mechanism. Now it uses pure OCaml code, without	ppedrot
2014-01-06	Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...	Arnaud Spiwack
2013-12-11	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot
2013-11-07	Rewriting the proof monad mechanism. Now it uses pure OCaml code, without	ppedrot
2013-11-02	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack