diff options
| author | herbelin | 2002-12-10 09:54:38 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-10 09:54:38 +0000 |
| commit | ba268db78c86f9ca0ccdb2524193e5346f7155b3 (patch) | |
| tree | f728a945fb3ee5ceef238a0a5f1afb67a68a5731 /kernel/term_typing.ml | |
| parent | c25437ecaac7edd4d5547c9e9c5fb05e54b31b21 (diff) | |
Déplacement du hash-consing vers declare.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1145ee94b0..0860b95eed 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -29,7 +29,11 @@ let constrain_type env j cst1 = function let cst3 = try conv_leq env j.uj_type tj.utj_val with NotConvertible -> error_actual_type env j tj.utj_val in - tj.utj_val, Constraint.union (Constraint.union cst1 cst2) cst3 + 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 let translate_local_def env (b,topt) = |