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/indschemes.ml | |
parent | 017d5133d8ec7339bf8170c98822638a58b66b14 (diff) | |
parent | e0a0159d7219a3d7e81f46001dcb2fdf1b466f8f (diff) |
Merge PR #7801: [vernac] Add option to force building really mutual induction schemes
Diffstat (limited to 'vernac/indschemes.ml')
-rw-r--r-- | vernac/indschemes.ml | 4 |
1 files changed, 2 insertions, 2 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 |