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

1 files changed, 20 insertions, 4 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3cf5cfd73..ce0677cae 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."))