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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10877 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretyping.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 19df941b2..0c03d1b6a 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 -- cgit v1.2.3