diff options
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 88de140dfa..31dd7e08a0 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 = |