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

3 files changed, 38 insertions, 6 deletions

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index e909a1f4fc..515b184daf 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -44,7 +44,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "strict mode";
-      optkey   = (SecondaryTable ("Strict","Proofs"));
+      optkey   = ["Strict";"Proofs"];
       optread  = get_strictness;
       optwrite = set_strictness }
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3cf5cfd736..ce0677caef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -44,6 +44,19 @@ open Clenv
 open Clenvtac
 open Evd
 
+(* Options *)
+
+let discr_do_intro = ref true
+
+open Goptions
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "automatic introduction of hypotheses by discriminate";
+      optkey   = ["Discriminate";"Introduction"];
+      optread  = (fun () -> !discr_do_intro);
+      optwrite = (:=) discr_do_intro }
+
 (* Rewriting tactics *)
 
 type orientation = bool
@@ -676,10 +689,13 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars)
 
 let discrEverywhere with_evars = 
   tclORELSE
-    (tclTHEN
-      (tclREPEAT introf) 
-      (Tacticals.tryAllHyps
-        (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
+    (if !discr_do_intro then
+      (tclTHEN
+	(tclREPEAT introf) 
+	(Tacticals.tryAllHyps
+          (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
+     else (* <= 8.2 compat *)
+       Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars))
     (fun gls -> 
        errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 099d60c090..bbc1285e2b 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