diff options
author | 2017-03-24 16:15:32 +0100 | |
---|---|---|
committer | 2017-03-24 16:15:32 +0100 | |
commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /intf | |
parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) |
Merge branch 'trunk' into pr379
Diffstat (limited to 'intf')
-rw-r--r-- | intf/misctypes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index e4f595ac4..33dc2a335 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 |