From d629ec7cd920b19a063b7198d4e5b92d91a5656b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Dec 2016 18:14:45 +0100
Subject: 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.
---
 pretyping/unification.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index baa12db08a..318a0b2cd8 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 =
-- 
cgit v1.2.3