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
---
 pretyping/pretyping.ml | 4 +++-
 pretyping/termops.ml   | 5 +++++
 pretyping/termops.mli  | 2 ++
 3 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 19df941b28..0c03d1b6a3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -411,7 +411,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | App (f,args) ->
               let f = whd_evar (Evd.evars_of !evdref) f in
               begin match kind_of_term f with
-              | Ind _ (* | Const _ *) ->
+              | Ind _ | Const _
+		  when isInd f or has_polymorphic_type (destConst f)
+		    ->
 	          let sigma = evars_of !evdref in
 		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	          let t = Retyping.get_type_of env sigma c in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 124637e131..6d8946f440 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -877,6 +877,11 @@ let isGlobalRef c =
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
+let has_polymorphic_type c =
+  match (Global.lookup_constant c).Declarations.const_type with
+  | Declarations.PolymorphicArity _ -> true
+  | _ -> false
+
 (* nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ded85464e9..608a7d9dbd 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -237,6 +237,8 @@ val is_section_variable : identifier -> bool
 
 val isGlobalRef : constr -> bool
 
+val has_polymorphic_type : constant -> bool
+
 (* Combinators on judgments *)
 
 val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
-- 
cgit v1.2.3