diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-27 13:34:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-27 13:34:14 +0200 |
| commit | 47ad058a918cb0fa8fef70fd7bd95bcb9ca05ee2 (patch) | |
| tree | e635d65f22b2b0f67b90ee6dd4ab8f339a4e5947 /intf | |
| parent | 01b7de3a673eb89cea61442c4db721aad9520c9f (diff) | |
| parent | 7fd28dc95e3251a10617ddb6758cc00b8960f954 (diff) | |
Merge PR #7062: Slightly refining some error messages about unresolvable evars.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml index c5de383b2..c964ecf1f 100644 --- a/intf/evar_kinds.ml +++ b/intf/evar_kinds.ml @@ -21,6 +21,8 @@ type obligation_definition_status = Define of bool | Expand type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar +type subevar_kind = Domain | Codomain | Body + type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) @@ -34,4 +36,4 @@ type t = | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Id.t - | SubEvar of Evar.t + | SubEvar of subevar_kind option * Evar.t |