diff options
| -rw-r--r-- | API/API.mli | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 5 |
3 files changed, 8 insertions, 3 deletions
diff --git a/API/API.mli b/API/API.mli index 7ec3cbee3..2e1d077c7 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3696,7 +3696,7 @@ end module Retyping : (* reconstruct the type of a term knowing that it was already typechecked *) sig val get_type_of : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types - val get_sort_family_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family + val get_sort_family_of : ?truncation_style:bool -> ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family val expand_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.constr -> EConstr.constr list -> EConstr.constr val get_sort_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.t diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 9653b0eef..f8f086fad 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -183,7 +183,7 @@ let retype ?(polyprop=true) sigma = in type_of, sort_of, type_of_global_reference_knowing_parameters -let get_sort_family_of ~polyprop env sigma t = +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in let rec sort_family_of env t = match EConstr.kind sigma t with @@ -194,11 +194,13 @@ let get_sort_family_of ~polyprop env sigma t = if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else let t = type_of_global_reference_knowing_parameters env f args in Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType | _ -> Sorts.family (decomp_sort env sigma (type_of env t)) in sort_family_of env t diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index af86df499..6fdde9046 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -31,8 +31,11 @@ val get_type_of : val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> Sorts.family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment |