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/typeops.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/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 616349ba0..53f230baa 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -135,10 +135,10 @@ let extract_context_levels env = List.fold_left (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] -let make_polymorphic_if_arity env t = +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with - | Sort (Type u) -> + | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> let param_ccls = extract_context_levels env params in let s = { poly_param_levels = param_ccls; poly_level = u} in PolymorphicArity (params,s) |