diff options
| author | herbelin | 2006-10-30 23:05:29 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-30 23:05:29 +0000 |
| commit | 71a48bb529cbaa36bc53b2ec3b721235b2b2ec38 (patch) | |
| tree | 2596cf37f9dae251e1c355aaaa0889472fb1b442 /kernel/inductive.ml | |
| parent | 6011cfe0b6e4c8660ec490cef1039955a41443f0 (diff) | |
Débranchement du polymorphisme de sorte sur les définitions dans Type
(trop de problèmes à régler, comme par exemple des types identiques
qui se retrouvent dans des sortes disjointes, résultant en davantage
d'équations (eq Type(i) a b) et (eq Type(j) a b) avec i syntaxiquement
distinct de j, que Coq ne sait en général pas traiter -- i.e. ne sait
pas forcer i==j (cf contrib CatsInZF: échec du test "dependent" dans
"rewrite"); autre problème: le ralentissement du prouveur (logic.ml)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index fcb45befa0..274561f0ca 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -135,6 +135,8 @@ let actualize_decl_level env lev t = let sign,s = dest_arity env t in mkArity (sign,lev) +let polymorphism_on_non_applied_parameters = false + (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) let rec make_subst env = function @@ -154,15 +156,18 @@ let rec make_subst env = function let s = sort_as_univ (snd (dest_arity env a)) in let ctx,subst = make_subst env (sign, exp, args) in d::ctx, cons_subst u s subst - | (na,None,t)::sign, Some u::exp, [] -> + | (na,None,t as d)::sign, Some u::exp, [] -> (* No more argument here: we instantiate the type with a fresh level *) (* which is first propagated to the corresponding premise in the arity *) (* (actualize_decl_level), then to the conclusion of the arity (via *) (* the substitution) *) - let s = fresh_local_univ () in - let t = actualize_decl_level env (Type s) t in let ctx,subst = make_subst env (sign, exp, []) in - (na,None,t)::ctx, cons_subst u s subst + if polymorphism_on_non_applied_parameters then + let s = fresh_local_univ () in + let t = actualize_decl_level env (Type s) t in + (na,None,t)::ctx, cons_subst u s subst + else + d::ctx, subst | sign, [], _ -> (* Uniform parameters are exhausted *) sign,[] |