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

4 files changed, 23 insertions, 8 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 11d6ed093a..911ded641e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -413,7 +413,7 @@ module CoercionPrinting =
     let encode = coercion_of_reference
     let subst = subst_coe_typ
     let printer x = pr_global_env Idset.empty x
-    let key = Goptions.SecondaryTable ("Printing","Coercion")
+    let key = ["Printing";"Coercion"]
     let title = "Explicitly printed coercions: "
     let member_message x b =
       str "Explicit printing of coercion " ++ printer x ++
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b2e9f0e6b4..d43bc07803 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -74,7 +74,7 @@ module PrintingCasesMake =
 	if kn' == kn then obj else
 	  (kn',i), ints
     let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
-    let key = Goptions.SecondaryTable ("Printing",Test.field)
+    let key = ["Printing";Test.field]
     let title = Test.title
     let member_message x = Test.member_message (printer x)
     let synchronous = true
@@ -118,7 +118,7 @@ let force_wildcard () = !wildcard_value
 let _ = declare_bool_option 
 	  { optsync  = true;
 	    optname  = "forced wildcard";
-	    optkey   = SecondaryTable ("Printing","Wildcard");
+	    optkey   = ["Printing";"Wildcard"];
 	    optread  = force_wildcard;
 	    optwrite = (:=) wildcard_value }
 
@@ -128,7 +128,7 @@ let synthetize_type () = !synth_type_value
 let _ = declare_bool_option 
 	  { optsync  = true;
 	    optname  = "pattern matching return type synthesizability";
-	    optkey   = SecondaryTable ("Printing","Synth");
+	    optkey   = ["Printing";"Synth"];
 	    optread  = synthetize_type;
 	    optwrite = (:=) synth_type_value }
 
@@ -138,7 +138,7 @@ let reverse_matching () = !reverse_matching_value
 let _ = declare_bool_option 
 	  { optsync  = true;
 	    optname  = "pattern-matching reversibility";
-	    optkey   = SecondaryTable ("Printing","Matching");
+	    optkey   = ["Printing";"Matching"];
 	    optread  = reverse_matching;
 	    optwrite = (:=) reverse_matching_value }
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 14121d328e..45fbe3227b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -330,7 +330,7 @@ let is_predicate_explicitly_dep env pred arsign =
 	  srec (push_rel_assum (na,t) env) b arsign
       | Lambda (na,_,_), _ ->
 
-       (* The following code has impact on the introduction names
+       (* The following code has an impact on the introduction names
 	  given by the tactics "case" and "inversion": when the
 	  elimination is not dependent, "case" uses Anonymous for
 	  inductive types in Prop and names created by mkProd_name for
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index dcb5efae55..d48c002e22 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -122,6 +122,18 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 *)
 
+(* Option introduced and activated in Coq 8.3 *)
+let global_evars_pattern_unification_flag = ref true
+
+open Goptions
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "pattern-unification for existential variables in tactics";
+      optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
+      optread  = (fun () -> !global_evars_pattern_unification_flag);
+      optwrite = (:=) global_evars_pattern_unification_flag }
+
 type unify_flags = { 
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
@@ -146,6 +158,9 @@ let default_no_delta_unify_flags = {
   use_evars_pattern_unification = true;
 }
 
+let use_evars_pattern_unification flags =
+  !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification 
+
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
   | Some (VarKey id) -> named_body id env
@@ -231,13 +246,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		  (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
 
 	| App (f1,l1), _ when
-	    (isMeta f1 || flags.use_evars_pattern_unification && isEvar f1) &
+	    (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) &
 	    is_unification_pattern curenvnb f1 l1 cN &
 	    not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenvnb f1 l1 cN substn
 
 	| _, App (f2,l2) when
-	    (isMeta f2 || flags.use_evars_pattern_unification && isEvar f2) &
+	    (isMeta f2 || use_evars_pattern_unification flags && isEvar f2) &
 	    is_unification_pattern curenvnb f2 l2 cM &
 	    not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenvnb f2 l2 cM substn