From d9736dae4168927f735ca4f60b61a83929ae4435 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Sep 2014 22:26:18 +0200
Subject: Be more conservative and keep the use of eq_constr in pretyping/
 functions.

---
 proofs/clenv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5a7572eb23..3ef3466340 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -167,7 +167,7 @@ let clenv_assign mv rhs clenv =
     error "clenv_assign: circularity in unification";
   try
     if meta_defined clenv.evd mv then
-      if not (eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+      if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
@@ -480,7 +480,7 @@ let clenv_match_args bl clenv =
       (fun clenv (loc,b,c) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+          if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
-- 
cgit v1.2.3