diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-30 21:58:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-30 21:58:41 +0000 |
| commit | 4f9cf134a3763de4ec5a5720edb11bb1e6eca66b (patch) | |
| tree | 203910b0443b742497299abd7cca372dd3f9915d /kernel/cooking.ml | |
| parent | 2460302bdd21427b849770b692918f4451801e2b (diff) | |
Réutilisation de l'infrastructure pour le polymorphisme d'univers des
constantes qui avait été mise en place pour la 8.1gamma puis abandonné
pour cause entre autres d'inefficacité. Cette fois, on restreind le
polymorphisme au seul cas d'alias vers un inductif.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10877 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index cc5beb974..a5cda5d13 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -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,false) |