diff options
| author | Pierre-Marie Pédrot | 2019-02-17 14:27:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-17 14:27:26 +0100 |
| commit | a49077ef67b8e70696ecacc311fc3070d1b7b461 (patch) | |
| tree | 1d9adcfba5d77543a91140dbacbe975da00c213e /kernel/type_errors.mli | |
| parent | 9014e6544cb251f140636f774e95df4037d8d8f6 (diff) | |
| parent | ac7169182a970c33be2e33abd43be5bf19542e2c (diff) | |
Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 3e954d6a8e..4b832930e1 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -130,3 +130,6 @@ val error_elim_explain : Sorts.family -> Sorts.family -> arity_error val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a val error_undeclared_universe : env -> Univ.Level.t -> 'a + +val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error +val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error |