1 files changed, 21 insertions, 35 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c92c183d..63cdb378 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -198,11 +198,18 @@ type unify_flags = {
     (* (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 *)
+    (* This controls which constants are unfoldable; this is on for apply *)
     (* (but not simple apply) since Feb 2008 for 8.2 *)
 
   modulo_delta_types : Names.transparent_state;
 
+  modulo_delta_in_merge : Names.transparent_state option;
+    (* This controls whether unfoldability is different when trying to unify *)
+    (* several instances of the same metavariable *)
+    (* Typical situation is when we give a pattern to be matched *)
+    (* syntactically against a subterm but we want the metas of the *)
+    (* pattern to be modulo convertibility *)
+
   check_applied_meta_types : bool;
     (* This controls whether meta's applied to arguments have their *)
     (* type unified with the type of their instance *)
@@ -240,12 +247,13 @@ type unify_flags = {
 }
 
 (* Default flag for unifying a type against a type (e.g. apply) *)
-(* We set all conversion flags *)
+(* We set all conversion flags (no flag should be modified anymore) *)
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = full_transparent_state;
   modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = None;
   check_applied_meta_types = true;
   resolve_evars = false;
   use_pattern_unification = true;
@@ -258,24 +266,22 @@ let default_unify_flags = {
       (* in fact useless when not used in w_unify_to_subterm_list *)
 }
 
+let set_merge_flags flags =
+  match flags.modulo_delta_in_merge with
+  | None -> flags
+  | Some ts ->
+    { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts }
+
 (* Default flag for the "simple apply" version of unification of a *)
 (* type against a type (e.g. apply) *)
 (* We set only the flags available at the time the new "apply" extends *)
 (* out of "simple apply" *)
-let default_no_delta_unify_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = true;
+let default_no_delta_unify_flags = { default_unify_flags with
   modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
-  restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
-  modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
 }
 
 (* Default flags for looking for subterms in elimination tactics *)
@@ -283,36 +289,16 @@ let default_no_delta_unify_flags = {
 (* allow_K) because only closed terms are involved in *)
 (* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
 (* 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_in_conv_on_closed_terms = true;
-  modulo_delta = full_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  check_applied_meta_types = true;
-  resolve_evars = false;
-  use_pattern_unification = true;
-  use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
+let elim_flags = { default_unify_flags with
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
-  modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = true
 }
 
-let elim_no_delta_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = true;
+let elim_no_delta_flags = { elim_flags with
   modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = false;
-  use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
-  restrict_conv_on_strict_subterms = false; (* ? *)
-  modulo_betaiota = false;
-  modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = true
 }
 
 let set_no_head_reduction flags =
@@ -865,7 +851,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	if Evd.is_defined evd evk then
 	  let v = Evd.existential_value evd ev in
 	  let (evd,metas',evars'') =
-	    unify_0 curenv evd CONV flags rhs v in
+	    unify_0 curenv evd CONV (set_merge_flags flags) rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
 	  (* This can make rhs' ill-typed if metas are *)
@@ -943,7 +929,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
-      unify_0 sp_env evd' CUMUL flags
+      unify_0 sp_env evd' CUMUL (set_merge_flags flags)
         (get_type_of sp_env evd' c) ev.evar_concl in
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''