diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.mli | 1 | ||||
| -rw-r--r-- | intf/misctypes.mli | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index afc5e3bab9..470ad2a23b 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -20,6 +20,7 @@ type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of obligation_definition_status | CasesType of bool (* true = a subterm of the type *) | InternalHole diff --git a/intf/misctypes.mli b/intf/misctypes.mli index e4f595ac4a..33dc2a335c 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -28,7 +28,7 @@ and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list - | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) + | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list |