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	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-07-28	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot
2014-07-24	Adding a tail-rec tclONCE.	Pierre-Marie Pédrot
2014-07-07	Revert "time tac" (committed by mistake).	Hugo Herbelin
2014-07-07	time tac	Hugo Herbelin
2014-04-20	Adding a [map] primitive to the tactic monad. Hopefully this should be	Pierre-Marie Pédrot
2014-04-07	Transfering the initial goals from the proofview to the proof object.	Pierre-Marie Pédrot
2014-04-06	Adding an [modify] function to the tactic monad. It allows to modify	Pierre-Marie Pédrot
2013-11-02	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