aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r--proofs/evar_refiner.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fb8e6b16e..8f7513371 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -17,9 +17,9 @@ open Evarutil
(******************************************)
let depends_on_evar evk _ (pbty,_,t1,t2) =
- try head_evar t1 = evk
+ try Int.equal (head_evar t1) evk
with NoHeadEvar ->
- try head_evar t2 = evk
+ try Int.equal (head_evar t2) evk
with NoHeadEvar -> false
let define_and_solve_constraints evk c evd =