diff options
| author | Arnaud Spiwack | 2014-01-06 10:44:32 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-01-06 10:44:32 +0100 |
| commit | 3525f2a01cd4f28882b721f40659d5c104e3077c (patch) | |
| tree | dd105f15275f686da3910c6a9f97fc282047c3aa /dev/base_include | |
| parent | 079829eb0b4a2875512b73310022cacee67366d0 (diff) | |
Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, without"
This reverts commit bfe1141026da70d8f59cf47b5fe61ffc20a29f3c.
Conflicts:
proofs/proofview_monad.ml
This is potentially a temporary commit until a final decision is taken on hand-written versus extracted ocaml for the tactic monad. The hand-written implementation has a bug where the + tactical would not behave properly (I tried to find why, but couldn't: the hand-written implementation looks fine, but it isn't. Beats me).
There is a conflict with Pierre-Marie's commit 4832692: Fixing backtrace registering of various tactic-related try-with blocks.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions