aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview_monad.ml
Commit message (Expand)AuthorAge
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutGravatar ppedrot2014-05-06
* Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...Gravatar Arnaud Spiwack2014-01-06
* Fixing backtrace registering of various tactic-related try-with blocks.Gravatar Pierre-Marie Pédrot2013-12-11
* Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutGravatar ppedrot2013-11-07
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...Gravatar aspiwack2013-11-02