From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 02:45:54 +0100
Subject: Hints API using EConstr.

---
 pretyping/evarsolve.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4ce8a44adc..7725719261 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1612,12 +1612,14 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
  * ass.
  *)
 
-let status_changed lev (pbty,_,t1,t2) =
-  (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
-  (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
+let status_changed evd lev (pbty,_,t1,t2) =
+  let t1 = EConstr.of_constr t1 in
+  let t2 = EConstr.of_constr t2 in
+  (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) ||
+  (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false)
 
 let reconsider_conv_pbs conv_algo evd =
-  let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
+  let (evd,pbs) = extract_changed_conv_pbs evd (status_changed evd) in
   List.fold_left
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
-- 
cgit v1.2.3