diff options
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 |