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

5 files changed, 25 insertions, 15 deletions

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