diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-08 16:17:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-08 16:17:52 +0000 |
| commit | 4a920351d9b68dc02ec45bf9fe67769dd0a8d3b2 (patch) | |
| tree | cb4fdd069f4f78626d6fbe865ed2ead31dfc646f /kernel | |
| parent | f1eaf5a1734e9716be089b2c8ebd14c6d2ec7684 (diff) | |
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
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 360d3d94c..b62e7b007 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) = |