diff options
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 3d9a344ee9..390711fabd 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -16,20 +16,22 @@ type patvar = Id.t (** Introduction patterns *) -type intro_pattern_expr = +type 'constr intro_pattern_expr = | IntroForthcoming of bool | IntroNaming of intro_pattern_naming_expr - | IntroAction of intro_pattern_action_expr + | IntroAction of 'constr intro_pattern_action_expr and intro_pattern_naming_expr = | IntroWildcard | IntroIdentifier of Id.t | IntroFresh of Id.t | IntroAnonymous -and intro_pattern_action_expr = - | IntroOrAndPattern of or_and_intro_pattern_expr - | IntroInjection of (Loc.t * intro_pattern_expr) list +and 'constr intro_pattern_action_expr = + | 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) | IntroRewrite of bool -and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list +and 'constr or_and_intro_pattern_expr = + (Loc.t * 'constr intro_pattern_expr) list list (** Move destination for hypothesis *) |