diff options
| author | Hugo Herbelin | 2017-11-28 19:45:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-28 19:48:55 +0100 |
| commit | 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (patch) | |
| tree | 9cfec2542b673e85dc04e340db656e8a3a98dc68 /API | |
| parent | 9348b4e69738c36a49e61a23a75a55c0e51f8fb7 (diff) | |
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.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 7ec3cbee3b..2e1d077c74 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 |