coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding an unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
*	Update headers.	Maxime Dénès	2015-01-12
*	Info: do not record info trace unless needed.	Arnaud Spiwack	2014-11-01
*	An API for info traces.	Arnaud Spiwack	2014-11-01
*	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-22
*	Refactoring proofview: make the definition of the logic monad polymorphic.	Arnaud Spiwack	2014-10-16
*	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