aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 16:15:32 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 16:15:32 +0100
commitaf291869bb7d1184d8e655906572d75937ca829b (patch)
tree62a5ccf9ee7b115b7d1118cbc3db92c553261713 /intf
parent3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff)
parent7535e268f7706d1dee263fdbafadf920349103db (diff)
Merge branch 'trunk' into pr379
Diffstat (limited to 'intf')
-rw-r--r--intf/misctypes.mli2
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