aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-18 11:36:05 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-12-12 13:30:57 +0100
commitc1cab3ba606f7034f2785f06c0d3892bca3976cf (patch)
tree19918420f7e4b64be31953dae8f51c981e638f4a /intf
parent745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 (diff)
Removing cumbersome location in multiple patterns.
This is to have a better symmetry between CCases and GCases.
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index e0d2d7bf4..8bcdbcc0e 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -104,7 +104,7 @@ and case_expr = constr_expr (* expression that is being matched
* cases_pattern_expr option (* in-clause *)
and branch_expr =
- (cases_pattern_expr list Loc.located list * constr_expr) Loc.located
+ (cases_pattern_expr list list * constr_expr) Loc.located
and binder_expr =
Name.t Loc.located list * binder_kind * constr_expr