diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 164fd60c9e..7d9599032b 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -18,6 +18,7 @@ type patvar = Id.t type intro_pattern_expr = | IntroOrAndPattern of or_and_intro_pattern_expr + | IntroInjection of (Loc.t * intro_pattern_expr) list | IntroWildcard | IntroRewrite of bool | IntroIdentifier of Id.t |