diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
| commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
| tree | 1a46f0142a85df553388c932110793881f3af52f /kernel/cooking.ml | |
| parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) | |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 02330339..ae717353 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -135,6 +135,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 @@ -145,4 +149,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) |