From 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 Nov 2017 19:45:31 +0100 Subject: Adding a variant get_truncation_family_of of get_sort_family_of. This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type. --- API/API.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'API') 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 -- cgit v1.2.3