Generalizing flag use_evars_pattern_unification into a flag

use_pattern_unification common for evars and metas. As a compensation,
add a flag use_meta_bound_pattern_unification to restore the old
mechanism of pattern unification for metas applied to rels only (this
is used e.g. by auto). Not sure yet, what could be the most
appropriate set of flags.  Added documentation of the flags.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 105 insertions, 38 deletions

diff --git a/CHANGES b/CHANGES
index 511c057f3f..10b0f09cf0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -33,6 +33,9 @@ Tactics
   result in some rare incompatibilities (solvable by adapting name hypotheses).
 - Introduction pattern "_" made more robust.
 - Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
+- Unification in "apply" supports unification of patterns of the form
+  ?f x y = g(x,y) (compatibility ensured by using
+  "Unset Tactic Pattern Unification").
 
 Vernacular commands
 
diff --git a/lib/flags.ml b/lib/flags.ml
index e8763bc79f..b9965af5dd 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -36,7 +36,7 @@ let raw_print = ref false
 
 (* Compatibility mode *)
 
-type compat_version = V8_2
+type compat_version = V8_2 | V8_3
 let compat_version = ref None
 let version_strictly_greater v =
   match !compat_version with None -> true | Some v' -> v'>v
diff --git a/lib/flags.mli b/lib/flags.mli
index f7e3c17597..4fd042e225 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -25,7 +25,7 @@ val load_proofs : load_proofs ref
 
 val raw_print : bool ref
 
-type compat_version = V8_2
+type compat_version = V8_2 | V8_3
 val compat_version : compat_version option ref
 val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5a2dfead7c..79debed864 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -156,29 +156,71 @@ let _ =
       optread  = (fun () -> !global_evars_pattern_unification_flag);
       optwrite = (:=) global_evars_pattern_unification_flag }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "pattern-unification for existential variables in tactics";
+      optkey   = ["Tactic";"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;
+    (* What this flag controls was activated with all constants transparent, *)
+    (* even for auto, since Coq V5.10 *)
+
+  use_metas_eagerly_in_conv_on_closed_terms : bool;
+    (* This refinement of the conversion on closed terms is activable *)
+    (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
+
   modulo_delta : Names.transparent_state;
+    (* This controls which constant are unfoldable; this is on for apply *)
+    (* (but not simple apply) since Feb 2008 for 8.2 *)
+
   modulo_delta_types : Names.transparent_state;
+
   resolve_evars : bool;
-  use_evars_pattern_unification : bool;
+    (* This says if type classes instances resolution must be used to infer *)
+    (* the remaining evars *)
+
+  use_pattern_unification : bool;
+    (* This says if type classes instances resolution must be used to infer *)
+    (* the remaining evars *)
+
+  use_meta_bound_pattern_unification : bool;
+    (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *)
+    (* This allows for instance to unify "forall x:A, B(x)" with "A' -> B'" *)
+    (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *)
+
   frozen_evars : ExistentialSet.t;
+    (* Evars of this set are considered axioms and never instantiated *)
+    (* Useful e.g. for autorewrite *)
+
   restrict_conv_on_strict_subterms : bool;
+    (* No conversion at the root of the term; potentially useful for rewrite *)
+
   modulo_betaiota : bool;
+    (* Support betaiota in the reduction *)
+    (* Note that zeta is always used *)
+
   modulo_eta : bool;
+    (* Support eta in the reduction *)
+
   allow_K_in_toplevel_higher_order_unification : bool
+    (* This is used only in second/higher order unification when looking for *)
+    (* subterms (rewrite and elim) *)
 }
 
 (* Default flag for unifying a type against a type (e.g. apply) *)
 (* We set all conversion flags *)
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = full_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
-  use_evars_pattern_unification = true;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;
@@ -193,11 +235,12 @@ let default_unify_flags = {
 (* out of "simple apply" *)
 let default_no_delta_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
-  use_evars_pattern_unification = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
@@ -212,11 +255,12 @@ let default_no_delta_unify_flags = {
 (* call w_unify for induction/destruct/case/elim  (13/6/2011) *)
 let elim_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = full_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
-  use_evars_pattern_unification = true;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
@@ -226,11 +270,12 @@ let elim_flags = {
 
 let elim_no_delta_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
-  use_evars_pattern_unification = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
@@ -242,9 +287,15 @@ let set_no_head_reduction flags =
   { flags with restrict_conv_on_strict_subterms = true }
 
 let use_evars_pattern_unification flags =
-  !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification
+  !global_evars_pattern_unification_flag && flags.use_pattern_unification
   && Flags.version_strictly_greater Flags.V8_2
 
+let use_metas_pattern_unification flags nb l =
+  !global_evars_pattern_unification_flag && flags.use_pattern_unification
+  || (Flags.version_less_or_equal Flags.V8_3 || 
+      flags.use_meta_bound_pattern_unification) &&
+     array_for_all (fun c -> isRel c && destRel c <= nb) l
+
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
   | Some (VarKey id) -> (try named_body id env with Not_found -> None)
@@ -355,15 +406,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	       reduce curenvnb pb b substn cM cN)
 
 	| App (f1,l1), _ when
-	    (isMeta f1 || use_evars_pattern_unification flags &&
-                          isAllowedEvar flags f1) &
+	    (isMeta f1 && use_metas_pattern_unification flags (snd curenvnb) l1
+             || use_evars_pattern_unification flags && isAllowedEvar flags 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 || use_evars_pattern_unification flags &&
-                          isAllowedEvar flags f2) &
+	    (isMeta f2 && use_metas_pattern_unification flags (snd curenvnb) l2
+             || use_evars_pattern_unification flags && isAllowedEvar flags f2) &
 	    is_unification_pattern curenvnb f2 l2 cM &
 	    not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenvnb f2 l2 cM substn
@@ -429,10 +480,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	 (it is used by apply and rewrite); it might now be redundant
 	 with the support for delta-expansion (which is used
 	 essentially for apply)... *)
+      not (subterm_restriction b flags) &&
       match flags.modulo_conv_on_closed_terms with
       | None -> false
-      | Some convflags when not (subterm_restriction b flags) ->
-      let subst = if flags.use_metas_eagerly then metasubst else ms in
+      | Some convflags ->
+      let subst = if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms in
       match subst_defined_metas subst cM with
       | None -> (* some undefined Metas in cM *) false
       | Some m1 ->
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 44b1c3889c..37eaa58026 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -12,11 +12,12 @@ open Evd
 
 type unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
-  use_metas_eagerly : bool;
+  use_metas_eagerly_in_conv_on_closed_terms : bool;
   modulo_delta : Names.transparent_state;
   modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
-  use_evars_pattern_unification : bool;
+  use_pattern_unification : bool;
+  use_meta_bound_pattern_unification : bool;
   frozen_evars : ExistentialSet.t;
   restrict_conv_on_strict_subterms : bool;
   modulo_betaiota : bool;
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index a266405f7a..ec9aada73c 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -102,11 +102,12 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
 
 let fail_quick_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = false;
+  use_metas_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
-  use_evars_pattern_unification = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true; (* ? *)
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 18e71661ff..af9420a245 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -840,11 +840,12 @@ open Unification
 
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = false;
+  use_metas_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = true;
-  use_evars_pattern_unification = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false; (* Compat *)
   modulo_betaiota = false;
@@ -971,7 +972,7 @@ and my_find_search mod_delta =
   else my_find_search_nodelta
 
 and my_find_search_delta db_list local_db hdc concl =
-  let flags = {auto_unif_flags with use_metas_eagerly = true} in
+  let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in
   let f = hintmap_of hdc concl in
     if occur_existential concl then
       list_map_append
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b460222b95..aed9f59857 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -74,11 +74,12 @@ open Unification
 
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = var_full_transparent_state;
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
-  use_evars_pattern_unification = true;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = true;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d2970603ea..3a40994f8c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -82,11 +82,12 @@ type conditions =
 
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
-  Unification.use_metas_eagerly = true;
+  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = empty_transparent_state;
   Unification.resolve_evars = true;
-  Unification.use_evars_pattern_unification = true;
+  Unification.use_pattern_unification = true;
+  Unification.use_meta_bound_pattern_unification = true;
   Unification.frozen_evars = ExistentialSet.empty;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
@@ -142,17 +143,19 @@ let rewrite_conv_closed_unif_flags = {
     (* We have this flag for historical reasons, it has e.g. the consequence *)
     (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
 
-  Unification.use_metas_eagerly = true;
+  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
     (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
     (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
 
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
   Unification.resolve_evars = false;
-  Unification.use_evars_pattern_unification = true;
+  Unification.use_pattern_unification = true;
     (* To rewrite "?n x y" in "y+x=0" when ?n is *)
     (* a preexisting evar of the goal*)
 
+  Unification.use_meta_bound_pattern_unification = true;
+
   Unification.frozen_evars = ExistentialSet.empty;
     (* This is set dynamically *)
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 821284ec7f..5400827bcf 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -302,11 +302,12 @@ let rewrite_transparent_state () =
 
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
-  Unification.use_metas_eagerly = true;
+  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
   Unification.resolve_evars = true;
-  Unification.use_evars_pattern_unification = true;
+  Unification.use_pattern_unification = true;
+  Unification.use_meta_bound_pattern_unification = true;
   Unification.frozen_evars = ExistentialSet.empty;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
@@ -316,11 +317,12 @@ let rewrite_unif_flags = {
 
 let rewrite2_unif_flags = 
   {  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
-     Unification.use_metas_eagerly = true;
+     Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
      Unification.modulo_delta = empty_transparent_state;
      Unification.modulo_delta_types = conv_transparent_state;
      Unification.resolve_evars = true;
-     Unification.use_evars_pattern_unification = true;
+     Unification.use_pattern_unification = true;
+     Unification.use_meta_bound_pattern_unification = true;
      Unification.frozen_evars = ExistentialSet.empty;
      Unification.restrict_conv_on_strict_subterms = false;
      Unification.modulo_betaiota = true;
@@ -331,11 +333,12 @@ let rewrite2_unif_flags =
 let general_rewrite_unif_flags () = 
   let ts = rewrite_transparent_state () in
     {  Unification.modulo_conv_on_closed_terms = Some ts;
-       Unification.use_metas_eagerly = true;
+       Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
        Unification.modulo_delta = ts;
        Unification.modulo_delta_types = ts;
        Unification.resolve_evars = true;
-       Unification.use_evars_pattern_unification = true;
+       Unification.use_pattern_unification = true;
+       Unification.use_meta_bound_pattern_unification = true;
        Unification.frozen_evars = ExistentialSet.empty;
        Unification.restrict_conv_on_strict_subterms = false;
        Unification.modulo_betaiota = true;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 060cd94a87..97928c87c2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -842,6 +842,7 @@ type conjunction_status =
 let make_projection sigma params cstr sign elim i n c =
   let elim = match elim with
   | NotADefinedRecordUseScheme elim ->
+      (* bugs: goes from right to left when i increases! *)
       let (na,b,t) = List.nth cstr.cs_args i in
       let b = match b with None -> mkRel (i+1) | Some b -> b in
       let branch = it_mkLambda_or_LetIn b cstr.cs_args in
@@ -856,6 +857,7 @@ let make_projection sigma params cstr sign elim i n c =
       else
 	None
   | DefinedRecord l ->
+      (* goes from left to right when i increases! *)
       match List.nth l i with
       | Some proj ->
 	  let t = Typeops.type_of_constant (Global.env()) proj in