diff options
| author | Pierre-Marie Pédrot | 2020-05-12 12:02:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 12:07:43 +0200 |
| commit | d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 (patch) | |
| tree | fa0648deb47650cc0d026ecdd711c093d36e585c /pretyping/inductiveops.mli | |
| parent | e802f48faf7a472000e218c7a3321c10c2171e0f (diff) | |
Do not use Unsafe.to_constr for old refiner conclusion.
This was useless, since we did not observe the difference on evars.
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 |