From 71a48bb529cbaa36bc53b2ec3b721235b2b2ec38 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 30 Oct 2006 23:05:29 +0000
Subject: 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
---
 kernel/inductive.ml   | 13 +++++++++----
 kernel/term_typing.ml |  3 +++
 2 files changed, 12 insertions(+), 4 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3