[vernac] Add option to force building really mutual induction schemes

Currently, if one of the inductives is non recursive, it defaults to a
case analysis schems taking fewer predicates and methods just for that
inductive. This irregularity prevents doing a combined scheme afterwards
to gather all eliminators into one, as combined scheme expects all the
eliminators to have the same predicates and methods. I have a use case
in building function graphs in Equations where some of the inductives
might not be recursive but I expect many other use cases could exist.

4 files changed, 14 insertions, 9 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 27b029aad..4ab932723 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
 
 (* Main function *)
-let mis_make_indrec env sigma listdepkind mib u =
+let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let evdref = ref sigma in
@@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u =
     (* Body on make_one_rec *)
     let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in
 
-      if (mis_is_recursive_subset
+      if force_mutual || (mis_is_recursive_subset
 	(List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind)
 	mipi.mind_recargs)
       then
@@ -558,7 +558,7 @@ let check_arities env listdepkind =
 	    [] listdepkind
   in true
 
-let build_mutual_induction_scheme env sigma = function
+let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
       if dep && not (Inductiveops.has_dependent_elim mib) then
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
 	   lrecspec)
       in
       let _ = check_arities env listdepkind in
-      mis_make_indrec env sigma listdepkind mib u
+      mis_make_indrec env sigma ~force_mutual listdepkind mib u
   | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.")
 
 let build_induction_scheme env sigma pind dep kind =
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index d87a19d28..de9d3a0ab 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive ->
 (** Builds mutual (recursive) induction schemes *)
 
 val build_mutual_induction_scheme :
-  env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
+  env -> evar_map -> ?force_mutual:bool ->
+  (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
 
 (** Scheme combinators *)
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2deca1e06..e86e10877 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -370,7 +370,7 @@ requested
 	| InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
 	| EqualityScheme  x -> l1,((None,smart_global_inductive x)::l2)
 
-let do_mutual_induction_scheme lnamedepindsort =
+let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
   let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort
   and env0 = Global.env() in
   let sigma, lrecspec, _ =
@@ -388,7 +388,7 @@ let do_mutual_induction_scheme lnamedepindsort =
           (evd, (indu,dep,sort) :: l, inst))
     lnamedepindsort (Evd.from_env env0,[],None)
   in
-  let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+  let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma ~force_mutual lrecspec in
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 261c3d813..ebfc76de9 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -29,9 +29,13 @@ val declare_congr_scheme : inductive -> unit
 
 val declare_rewriting_schemes : inductive -> unit
 
-(** Mutual Minimality/Induction scheme *)
+(** Mutual Minimality/Induction scheme.
+    [force_mutual] forces the construction of eliminators having the same predicates and
+    methods even if some of the inductives are not recursive.
+    By default it is [false] and some of the eliminators are defined as simple case analysis.
+ *)
 
-val do_mutual_induction_scheme :
+val do_mutual_induction_scheme : ?force_mutual:bool ->
   (lident * bool * inductive * Sorts.family) list -> unit
 
 (** Main calls to interpret the Scheme command *)