diff options
| author | Emilio Jesus Gallego Arias | 2020-05-13 02:49:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-13 02:49:27 +0200 |
| commit | 4a5944448e31022593df7d6e7e0318cfea92ea98 (patch) | |
| tree | 643d10e4058af9db9efbf84d7c91c4d8eeb152e1 /pretyping/inductiveops.mli | |
| parent | 0992c2669324a2ab911f5a4c08c27dc97f2bf371 (diff) | |
| parent | c5fdfe6ffef15795ecfde8f18f332ddefd35605e (diff) | |
Merge PR #12307: Cleaning up the legacy proof engine
Reviewed-by: ejgallego
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 ab69629595..2bec86599e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,7 +194,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : - env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> EConstr.types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info |