aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview_monad.ml
AgeCommit message (Expand)Author
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutppedrot
2014-01-06Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...Arnaud Spiwack
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-11-07Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutppedrot
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...aspiwack