From e0a0159d7219a3d7e81f46001dcb2fdf1b466f8f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 13 Jun 2018 22:54:25 +0200 Subject: [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. --- vernac/indschemes.ml | 4 ++-- vernac/indschemes.mli | 8 ++++++-- 2 files changed, 8 insertions(+), 4 deletions(-) (limited to 'vernac') 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 *) -- cgit v1.2.3