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.

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