Renaming to more generic has_dependent_elim test

4 files changed, 15 insertions, 13 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 *)
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index ecee2e540..f9e6c207c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind =
   let kind = inductive_sort_family mip in
   let dep =
     if kind == InProp then case_scheme_kind_from_prop
-    else if Inductiveops.is_primitive_record_without_eta mib then
+    else if not (Inductiveops.has_dependent_elim mib) then
       case_scheme_kind_from_type
     else case_dep_scheme_kind_from_type in
   let kelim = elim_sorts (mib,mip) in
@@ -250,14 +250,14 @@ let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
   let from_prop = kind == InProp in
-  let primwithouteta = Inductiveops.is_primitive_record_without_eta mib in
+  let depelim = Inductiveops.has_dependent_elim mib in
   let kelim = elim_sorts (mib,mip) in
   let elims =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop
-       else if primwithouteta then nondep_kinds_from_type
-       else kinds_from_type) in
+       else if depelim then kinds_from_type
+       else nondep_kinds_from_type) in
   List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims