Term_typing, Typeops: replace some generic '=' on constr by eq_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14313 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 3 insertions, 3 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 6b44bcad3..2c784e00e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -32,7 +32,7 @@ let constrain_type env j cst1 = function
   | Some t ->
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-	assert (t = tj.utj_val);
+	assert (eq_constr t tj.utj_val);
 	let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
 	  NonPolymorphicType t, cstrs
 
@@ -42,7 +42,7 @@ let local_constrain_type env j cst1 = function
   | Some t ->
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-      assert (t = tj.utj_val);
+      assert (eq_constr t tj.utj_val);
       t, union_constraints (union_constraints cst1 cst2) cst3
 
 let translate_local_def env (b,topt) =
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 85e8e6c88..c9112e86d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -475,7 +475,7 @@ and execute_array env = array_fold_map' (execute env)
 let infer env constr =
   let (j,(cst,_)) =
     execute env constr (empty_constraint, universes env) in
-  assert (j.uj_val = constr);
+  assert (eq_constr j.uj_val constr);
   ({ j with uj_val = constr }, cst)
 
 let infer_type env constr =