diff options
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 |