Putting back the occur_meta_or_undefined_evar function in the old term API.

This is another perfomance-critical function in unification. Putting it in
the EConstr API was changing the heuristic, so better revert on that change.

1 files changed, 10 insertions, 3 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index baa12db08..318a0b2cd 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -65,10 +65,17 @@ let _ = Goptions.declare_bool_option {
 }
 
 let occur_meta_or_undefined_evar evd c =
-  let rec occrec c = match EConstr.kind evd c with
+  (** This is performance-critical. Using the evar-insensitive API changes the
+      resulting heuristic. *)
+  let c = EConstr.Unsafe.to_constr c in
+  let rec occrec c = match kind_of_term c with
     | Meta _ -> raise Occur
-    | Evar _ -> raise Occur
-    | _ -> EConstr.iter evd occrec c
+    | Evar (ev,args) ->
+        (match evar_body (Evd.find evd ev) with
+        | Evar_defined c ->
+            occrec c; Array.iter occrec args
+        | Evar_empty -> raise Occur)
+    | _ -> Constr.iter occrec c
   in try occrec c; false with Occur | Not_found -> true
 
 let occur_meta_evd sigma mv c =