diff options
author | 2012-07-11 16:42:09 +0000 | |
---|---|---|
committer | 2012-07-11 16:42:09 +0000 | |
commit | df954f17d5f487e06ee21e10bab1ae9a133ba72d (patch) | |
tree | 18c5d0e64dc17792ca2537896cc70d92a16c3a34 /dev/printers.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 'dev/printers.mllib')
-rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index a6d93aa8c..45da00a72 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -126,6 +126,7 @@ Logic Refiner Clenv Evar_refiner +Monads Proofview Proof Proof_global |