Renaming to more generic has_dependent_elim test

3 files changed, 11 insertions, 9 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 012c97549..45eaae124 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -484,7 +484,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 let build_case_analysis_scheme env sigma pity dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  if dep && Inductiveops.is_primitive_record_without_eta mib then
+  if dep && not (Inductiveops.has_dependent_elim mib) then
     raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
@@ -495,7 +495,7 @@ let is_in_prop mip =
 
 let build_case_analysis_scheme_default env sigma pity kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in
+  let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 (**********************************************************************)
@@ -556,7 +556,7 @@ let check_arities env listdepkind =
 let build_mutual_induction_scheme env sigma = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
-      if dep && Inductiveops.is_primitive_record_without_eta mib then
+      if dep && not (Inductiveops.has_dependent_elim mib) then
         raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
       let (sp,tyi) = mind in
       let listdepkind =
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
 
 let build_induction_scheme env sigma pind dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pind) in
-  if dep && Inductiveops.is_primitive_record_without_eta mib then
+  if dep && not (Inductiveops.has_dependent_elim mib) then
     raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
   let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
     sigma, List.hd l
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 64932145e..e4f98e730 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,10 +269,10 @@ let projection_nparams_env env p =
 
 let projection_nparams p = projection_nparams_env (Global.env ()) p
 
-let is_primitive_record_without_eta mib =
+let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite
-  | _ -> false
+  | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+  | _ -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 6c49099a8..7ef848f0d 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -122,14 +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
 
-(** Recursive records with primitive projections do not have eta-conversion *)
-val is_primitive_record_without_eta : mutual_inductive_body -> bool
 
 (** Extract information from an inductive family *)