diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-11 16:42:09 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-11 16:42:09 +0000 |
| commit | df954f17d5f487e06ee21e10bab1ae9a133ba72d (patch) | |
| tree | 18c5d0e64dc17792ca2537896cc70d92a16c3a34 /proofs/proofs.mllib | |
| parent | e6bf1b6936f8bd61eb1266f7f4dd67181f3630f1 (diff) | |
Severe reorganisation of the code of tactics in Proofview.
All the purely monadic code has been moved to a new module Monads,
where, I'm afraid to confess, I got to use a number of proof transformers
to modularise the definition of tactics. It is still not easy to understand (why
would it with backtracking support?) but at least it's more robust, cleaner,
and more extensible. Plus there is now a Proofview.tclORELSE which will
be used to interprete the Ltac tactical (t1 || t2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15596 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proofs.mllib')
| -rw-r--r-- | proofs/proofs.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index ca0c7dd0d..96af73b71 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,5 +1,6 @@ Goal Evar_refiner +Monads Proofview Proof Proof_global |