diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5583eff4d..1561cf97b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -156,8 +156,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - (rel_context -> rel_context) -> env -> pinductive * constr list -> constr -> - constr -> types array * types + env -> pinductive * constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info |