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
*	Some comments in the interface of Proofview_monad.	Arnaud Spiwack	2014-08-04
*	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack	2014-08-04
*	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot	2014-07-28
*	Adding a tail-rec tclONCE.	Pierre-Marie Pédrot	2014-07-24
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Adding a [map] primitive to the tactic monad. Hopefully this should be	Pierre-Marie Pédrot	2014-04-20
*	Transfering the initial goals from the proofview to the proof object.	Pierre-Marie Pédrot	2014-04-07
*	Adding an [modify] function to the tactic monad. It allows to modify	Pierre-Marie Pédrot	2014-04-06
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	A dedicated view type for Proofview_gen.split.	aspiwack	2013-11-02
*	Makes the Ltac debugger usable again.	aspiwack	2013-11-02
*	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack	2013-11-02