diff options
Diffstat (limited to 'pretyping/indrec.mli')
| -rw-r--r-- | pretyping/indrec.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 *) |