diff options
| -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) = |