diff options
| author | herbelin | 2008-04-30 21:58:41 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-30 21:58:41 +0000 |
| commit | 4f9cf134a3763de4ec5a5720edb11bb1e6eca66b (patch) | |
| tree | 203910b0443b742497299abd7cca372dd3f9915d /pretyping | |
| parent | 2460302bdd21427b849770b692918f4451801e2b (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/termops.ml | 5 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 |
3 files changed, 10 insertions, 1 deletions
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 |