From 4f9cf134a3763de4ec5a5720edb11bb1e6eca66b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 30 Apr 2008 21:58:41 +0000
Subject: 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
---
 proofs/logic.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 67bb3a3c21..654bc504a9 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -278,8 +278,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  match kind_of_term f with
-	    | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
-		when not (array_exists occur_meta l) (* we could be finer *) ->
+	    | Ind _ | Const _
+		when not (array_exists occur_meta l) (* we could be finer *)
+		  & (isInd f or has_polymorphic_type (destConst f))
+		  ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
 		type_of_global_reference_knowing_parameters env sigma f l
-- 
cgit v1.2.3