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