diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 13:55:55 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 13:55:55 +0200 |
| commit | cd2af7f5dd96a639dbc531064d89de0ee82ef3e6 (patch) | |
| tree | 3d1beb40500380fb5f74cc50d23550f84d46a7a9 /vernac | |
| parent | 017d5133d8ec7339bf8170c98822638a58b66b14 (diff) | |
| parent | e0a0159d7219a3d7e81f46001dcb2fdf1b466f8f (diff) | |
Merge PR #7801: [vernac] Add option to force building really mutual induction schemes
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/indschemes.ml | 4 | ||||
| -rw-r--r-- | vernac/indschemes.mli | 8 |
2 files changed, 8 insertions, 4 deletions
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 *) |