From 4a920351d9b68dc02ec45bf9fe67769dd0a8d3b2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Nov 2005 16:17:52 +0000
Subject: Nettoyage suite nouvel avertissement Z de ocaml 3.09

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7535 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term_typing.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 360d3d94c0..b62e7b007a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -31,11 +31,8 @@ let constrain_type env j cst1 = function
       let cst3 =
 	try vm_conv_leq env j.uj_type tj.utj_val
 	with NotConvertible -> error_actual_type env j tj.utj_val in
-      let typ = 
-        if t = tj.utj_val then t else
-          (error "Kernel built a type different from its input\n";
-           flush stdout; tj.utj_val) in
-      typ, Constraint.union (Constraint.union cst1 cst2) cst3
+      assert (t = tj.utj_val);
+      t, Constraint.union (Constraint.union cst1 cst2) cst3
 
 
 let translate_local_def env (b,topt) =
-- 
cgit v1.2.3