diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 09:54:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 09:54:38 +0000 |
| commit | ba268db78c86f9ca0ccdb2524193e5346f7155b3 (patch) | |
| tree | f728a945fb3ee5ceef238a0a5f1afb67a68a5731 /kernel/typeops.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/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 88de140df..31dd7e08a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -444,6 +444,9 @@ and execute_list env l cu = let infer env constr = let (j,(cst,_)) = execute env constr (Constraint.empty, universes env) in + let j = if j.uj_val = constr then { j with uj_val = constr } else + (error "Kernel built a body different from its input\n"; + flush stdout; j) in (j, cst) let infer_type env constr = |