diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.ml | 4 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml index c5de383b21..c964ecf1f5 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 diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index df061bfb72..dc1110ad86 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -457,8 +457,6 @@ type nonrec vernac_expr = | VernacCheckGuard | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string - (* Toplevel control *) - | VernacToplevelControl of exn (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list |