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