summaryrefslogtreecommitdiff
path: root/kernel/cooking.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /kernel/cooking.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'kernel/cooking.ml')
-rw-r--r--kernel/cooking.ml10
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 6b2a6245..e5a97897 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cooking.ml 9320 2006-10-30 16:53:43Z barras $ i*)
+(*i $Id: cooking.ml 10877 2008-04-30 21:58:41Z herbelin $ i*)
open Pp
open Util
@@ -113,7 +113,7 @@ type recipe = {
d_modlist : work_list }
let on_body f =
- option_map (fun c -> Declarations.from_val (f (Declarations.force c)))
+ Option.map (fun c -> Declarations.from_val (f (Declarations.force c)))
let cook_constant env r =
let cb = r.d_from in
@@ -129,6 +129,8 @@ let cook_constant env r =
| PolymorphicArity (ctx,s) ->
let t = mkArity (ctx,Type s.poly_level) in
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
- Typeops.make_polymorphic_if_arity env typ in
+ let j = make_judge (force (Option.get body)) typ in
+ Typeops.make_polymorphic_if_constant_for_ind env j
+ in
let boxed = Cemitcodes.is_boxed cb.const_body_code in
- (body, typ, cb.const_constraints, cb.const_opaque, boxed)
+ (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)