coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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	2013-11-02