Fix strategy of Keyed Unification

Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.

1 files changed, 27 insertions, 3 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 55210d067..31fd711bf 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -356,6 +356,22 @@ let set_no_delta_flags flags = {
   resolve_evars = flags.resolve_evars
 }
 
+(* For the first phase of keyed unification, restrict
+  to conversion (including beta-iota) only on closed terms *)
+let set_no_delta_open_core_flags flags = { flags with
+  modulo_delta = empty_transparent_state;
+  modulo_betaiota = false;
+}
+
+let set_no_delta_open_flags flags = {
+  core_unify_flags = set_no_delta_open_core_flags flags.core_unify_flags;
+  merge_unify_flags = set_no_delta_open_core_flags flags.merge_unify_flags;
+  subterm_unify_flags = set_no_delta_open_core_flags flags.subterm_unify_flags;
+  allow_K_in_toplevel_higher_order_unification =
+      flags.allow_K_in_toplevel_higher_order_unification;
+  resolve_evars = flags.resolve_evars
+}
+
 (* 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" extended *)
@@ -1790,17 +1806,25 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
         let allow_K = flags.allow_K_in_toplevel_higher_order_unification in
         let flags =
           if occur_meta_or_existential op || !keyed_unification then
+	    (* This is up to delta for subterms w/o metas ... *)
             flags
           else
             (* up to Nov 2014, unification was bypassed on evar/meta-free terms;
                now it is called in a minimalistic way, at least to possibly
                unify pre-existing non frozen evars of the goal or of the
                pattern *)
-            set_no_delta_flags flags in
+          set_no_delta_flags flags in
+	let t' = (strip_outer_cast op,t) in
         let (evd',cl) =
           try
-	    (* This is up to delta for subterms w/o metas ... *)
-	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
+  	    if is_keyed_unification () then
+    	      try (* First try finding a subterm w/o conversion on open terms *)
+	        let flags = set_no_delta_open_flags flags in
+		w_unify_to_subterm env evd ~flags t'
+	      with e ->
+		(* If this fails, try with full conversion *)
+		w_unify_to_subterm env evd ~flags t'
+	    else w_unify_to_subterm env evd ~flags t'
 	  with PretypeError (env,_,NoOccurrenceFound _) when
               allow_K ||
                 (* w_unify_to_subterm does not go through evars, so