From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Nov 2016 20:35:01 +0100
Subject: Equality API using EConstr.

---
 engine/evarutil.ml | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4f40499d0a..c2ad3c4628 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -690,29 +690,26 @@ let rec advance sigma evk =
 
 let undefined_evars_of_term evd t =
   let rec evrec acc c =
-    match kind_of_term c with
+    match EConstr.kind evd c with
       | Evar (n, l) ->
-	let acc = Array.fold_left evrec acc l in
-	(try match (Evd.find evd n).evar_body with
-	  | Evar_empty -> Evar.Set.add n acc
-	  | Evar_defined c -> evrec acc c
-	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
-      | _ -> fold_constr evrec acc c
+        let acc = Evar.Set.add n acc in
+	Array.fold_left evrec acc l
+      | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
 
 let undefined_evars_of_named_context evd nc =
   Context.Named.fold_outside
-    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c))))
     nc
     ~init:Evar.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+  Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
     (Evar.Set.union
        (match evi.evar_body with
 	 | Evar_empty -> Evar.Set.empty
-	 | Evar_defined b -> undefined_evars_of_term evd b)
+	 | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
-- 
cgit v1.2.3