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

4 files changed, 17 insertions, 5 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,[]
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index d834504ab6..8b0f45ac9c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,7 +24,10 @@ open Typeops
 
 let constrain_type env j cst1 = function
   | None ->
+(* To have definitions in Type polymorphic
       make_polymorphic_if_arity env j.uj_type, cst1
+*) 
+      NonPolymorphicType j.uj_type, cst1
   | Some t -> 
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 33b22c3b73..f56a924756 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -292,7 +292,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  match kind_of_term f with
-	    | (Ind _ | Const _)
+	    | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
 		when not (array_exists occur_meta l) (* we could be finer *) ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index a49b927da7..5a008f18b5 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,8 +1,12 @@
 (* Some tests of sort-polymorphisme *)
 Section S.
 Variable A:Type.
+(*
 Definition f (B:Type) := (A * B)%type.
+*)
 Inductive I (B:Type) : Type := prod : A->B->I B.
 End S.
+(*
 Check f nat nat : Set.
+*)
 Check I nat nat : Set.