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.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'vernac/indschemes.mli') 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