fix unification and flags

Author: Tragicus

pretyping/evarconv.ml

@@ -705,10 +705,9 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
            destroy beta-redexes that can be used for 1st-order unification *)
         let term1 = apprec_nohdbeta flags env evd term1 in
         let term2 = apprec_nohdbeta flags env evd term2 in
-        let default () =
-          let hd1 = (whd_nored_state env evd (term1,Stack.empty)) in
-          let hd2 = (whd_nored_state env evd (term2,Stack.empty)) in
-        match
+        let hd1 = (whd_nored_state env evd (term1,Stack.empty)) in
+        let hd2 = (whd_nored_state env evd (term2,Stack.empty)) in
+        begin match
           evar_eqappr_x flags env evd pbty (Cs_keys_cache.empty ()) None
             { left = hd1; right = hd2 } hd1 hd2
         with
@@ -718,30 +717,6 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
            then Success evd
            else x
         | Success _ as x -> x
-        in
-          begin match EConstr.kind evd term1, EConstr.kind evd term2 with
-          | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
-            (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
-              (position_problem true pbty,ev,term2) with
-              | UnifFailure (_,(OccurCheck _ | NotClean _)) ->
-                (* Eta-expansion might apply *)
-                (* OccurCheck: eta-expansion could solve
-                     ?X = {| foo := ?X.(foo) |}
-                   NotClean: pruning in solve_simple_eqn is incomplete wrt
-                     Miller patterns *)
-                default ()
-              | x -> x)
-          | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
-            (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
-              (position_problem false pbty,ev,term1) with
-              | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
-                (* OccurCheck: eta-expansion could solve
-                     ?X = {| foo := ?X.(foo) |}
-                   NotClean: pruning in solve_simple_eqn is incomplete wrt
-                     Miller patterns *)
-                default ()
-              | x -> x)
-          | _ -> default ()
         end
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
@@ -752,13 +727,25 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     UnifFailure (i, NotSameHead)
   in
   let miller_pfenning l2r fallback ev lF tM evd =
-    match is_unification_pattern_evar env evd ev lF tM with
+    let r =
+      if lF = [] then
+        solve_simple_eqn (conv_fun evar_conv_x) flags env evd
+          (position_problem l2r pbty,ev,tM)
+      else UnifFailure (evd, OccurCheck (fst ev, tM)) in
+    match r with
+    | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
+      (* OccurCheck: eta-expansion could solve
+           ?X = {| foo := ?X.(foo) |}
+         NotClean: pruning in solve_simple_eqn is incomplete wrt
+           Miller patterns *)
+      (match is_unification_pattern_evar env evd ev lF tM with
       | None -> fallback ()
       | Some l1' -> (* Miller-Pfenning's patterns unification *)
         let t2 = tM in
         let t2 = solve_pattern_eqn env evd l1' t2 in
           solve_simple_eqn (conv_fun evar_conv_x) flags env evd
-            (position_problem l2r pbty,ev,t2)
+            (position_problem l2r pbty,ev,t2))
+    | r -> r
   in
   let consume_stack l2r (termF,skF) (termO,skO) evd =
     let switch f a b = if l2r then f a b else f b a in
@@ -803,6 +790,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     else quick_fail i
   in
   let miller l2r ev (termF,skF as apprF) (termM, skM as apprM) i =
+    let () = debug_unification (fun () -> Pp.(v 0 (str "miller " ++ pr_state env evd apprF ++ cut () ++ pr_state env evd apprM ++ cut ()))) in
     let switch f a b = if l2r then f a b else f b a in
     let not_only_app = Stack.not_purely_applicative skM in
       match Stack.list_of_app_stack skF with

pretyping/unification.ml

@@ -653,7 +653,7 @@ let default_unify_flags () =
 }
 
 let set_no_delta_core_flags flags = { flags with
-  modulo_conv_on_closed_terms = None;
+  modulo_conv_on_closed_terms = Some TransparentState.empty;
   modulo_delta = TransparentState.empty;
   check_applied_meta_types = false;
   use_pattern_unification = false;