diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 1a405e98ba..e79bc90bbc 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -136,6 +136,10 @@ let cook_constant env r = (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps) cb.const_body in + let const_hyps = + Sign.fold_named_context (fun (h,_,_) hyps -> + List.filter (fun (id,_,_) -> id <> h) hyps) + hyps ~init:cb.const_hyps in let typ = match cb.const_type with | NonPolymorphicType t -> let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in @@ -146,4 +150,4 @@ let cook_constant env r = let j = make_judge (constr_of_def body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in - (body, typ, cb.const_constraints) + (body, typ, cb.const_constraints, const_hyps) |