coq - The formal proof system

Age	Commit message (Expand)	Author
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
2014-02-02	Fixing backtrace reporting.	Pierre-Marie Pédrot
2014-01-30	Fixing backtrace handling here and there.	Pierre-Marie Pédrot
2013-11-02	Cleanup of comments in bootstrap/Monads.v	aspiwack
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	Adds a shelve tactic.	aspiwack
2013-11-02	bootstrap/Monad.v: implements the writer monad in continuation passing style.	aspiwack
2013-11-02	bootstrap/Monad.v: implements the environment monad in continuation passing s...	aspiwack
2013-11-02	Factors the lifting of environment and writer monads in bootstrap/Monad.v	aspiwack
2013-11-02	A dedicated view type for Proofview_gen.split.	aspiwack
2013-11-02	Typos in a comment.	aspiwack
2013-11-02	bootstrap/Monads.v: A more efficient split.	aspiwack
2013-11-02	State monad implemented in CPS.	aspiwack
2013-11-02	A more principled split.	aspiwack
2013-11-02	Set an extraction flag for inling let-s in Monad.v.	aspiwack
2013-11-02	Various rewriting, mostly for speed purposes.	aspiwack
2013-11-02	Optimisation of partial applications in the tactic monad.	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