aboutsummaryrefslogtreecommitdiffhomepage
path: root/bootstrap
Commit message (Expand)AuthorAge
* Fixing backtrace reporting.Gravatar Pierre-Marie Pédrot2014-02-02
* Fixing backtrace handling here and there.Gravatar Pierre-Marie Pédrot2014-01-30
* Cleanup of comments in bootstrap/Monads.vGravatar aspiwack2013-11-02
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* bootstrap/Monad.v: implements the writer monad in continuation passing style.Gravatar aspiwack2013-11-02
* bootstrap/Monad.v: implements the environment monad in continuation passing s...Gravatar aspiwack2013-11-02
* Factors the lifting of environment and writer monads in bootstrap/Monad.vGravatar aspiwack2013-11-02
* A dedicated view type for Proofview_gen.split.Gravatar aspiwack2013-11-02
* Typos in a comment.Gravatar aspiwack2013-11-02
* bootstrap/Monads.v: A more efficient split.Gravatar aspiwack2013-11-02
* State monad implemented in CPS.Gravatar aspiwack2013-11-02
* A more principled split.Gravatar aspiwack2013-11-02
* Set an extraction flag for inling let-s in Monad.v.Gravatar aspiwack2013-11-02
* Various rewriting, mostly for speed purposes.Gravatar aspiwack2013-11-02
* Optimisation of partial applications in the tactic monad.Gravatar aspiwack2013-11-02
* Makes the Ltac debugger usable again.Gravatar aspiwack2013-11-02
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...Gravatar aspiwack2013-11-02