Merge branch 'v8.6'

1 files changed, 14 insertions, 1 deletions

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index d25f8a8378..7bd616591f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -122,11 +122,16 @@ val inductive_has_local_defs : inductive -> bool
 
 val allowed_sorts : env -> inductive -> sorts_family list
 
+(** (Co)Inductive records with primitive projections do not have eta-conversion,
+    hence no dependent elimination. *)
+val has_dependent_elim : mutual_inductive_body -> bool
+
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
-  constr -> types -> types
+				     constr -> types -> types
+
 
 (** Extract information from an inductive family *)
 
@@ -175,6 +180,14 @@ val type_case_branches_with_names :
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info
 
+(** Make a case or substitute projections if the inductive type is a record
+    with primitive projections.
+    Fail with an error if the elimination is dependent while the
+    inductive type does not allow dependent elimination. *)
+val make_case_or_project :
+  env -> inductive_family -> case_info ->
+  (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr
+
 (*i Compatibility
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)