diff options
author | 2009-08-02 19:51:48 +0000 | |
---|---|---|
committer | 2009-08-02 19:51:48 +0000 | |
commit | 25dde2366a4db47e5da13b2bbe4d03a31235706f (patch) | |
tree | 5fe442297f6aabf515ce4aad817e31818fb4deb0 /tactics/tauto.ml4 | |
parent | 581223c7fc607b5121013928fd83606b82ea8531 (diff) |
Improved parameterization of Coq:
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tauto.ml4')
-rw-r--r-- | tactics/tauto.ml4 | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 099d60c09..bbc1285e2 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -45,6 +45,17 @@ let strict_in_hyp_and_ccl = false (* Whether unit type includes equality types *) let strict_unit = false +(* Whether inner iff are unfolded *) +let iff_unfolding = ref false + +open Goptions +let _ = + declare_bool_option + { optsync = true; + optname = "unfolding of iff and not in intuition"; + optkey = ["Intuition";"Iff";"Unfolding"]; + optread = (fun () -> !iff_unfolding); + optwrite = (:=) iff_unfolding } (** Test *) @@ -180,6 +191,7 @@ let simplif ist = (match reverse goal with | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.not _) |- _ => red in id | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id | id0: ?X1 -> ?X2, id1: ?X1|- _ => (* generalize (id0 id1); intro; clear id0 does not work @@ -204,6 +216,7 @@ let simplif ist = (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *) | |- ?X1 => $t_is_conj; split | |- (Coq.Init.Logic.iff _ _) => split + | |- (Coq.Init.Logic.not _) => red end; $t_not_dep_intros) >> @@ -236,7 +249,10 @@ let rec tauto_intuit t_reduce solver ist = ) >> let reduction_not _ist = - <:tactic< unfold Coq.Init.Logic.not in * >> + if !iff_unfolding then + <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >> + else + <:tactic< unfold Coq.Init.Logic.not in * >> let t_reduction_not = tacticIn reduction_not |