coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-09-04
*	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-05
*	Cleaning the new implementation of the tactic monad continued.	Arnaud Spiwack	2014-08-04
*	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-05-06
*	Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...	Arnaud Spiwack	2014-01-06
*	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot	2013-12-11
*	Rewriting the proof monad mechanism. Now it uses pure OCaml code, without	ppedrot	2013-11-07
*	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack	2013-11-02