aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-16 13:02:55 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-24 23:58:22 +0200
commitad3aab9415b98a247a6cbce05752632c3c42391c (patch)
tree1fba7e25aa16dbb7e42db283f8210b31a0b8931d /intf
parent6d9e008ffd81bbe927e3442fb0c37269ed25b21f (diff)
[location] Move Glob_term.cases_pattern to located.
We continue the uniformization pass. No big news here, trying to be minimally invasive.
Diffstat (limited to 'intf')
-rw-r--r--intf/glob_term.mli7
1 files changed, 4 insertions, 3 deletions
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ced5a8b44..5e771245c 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -24,10 +24,11 @@ type existential_name = Id.t
(** The kind of patterns that occurs in "match ... with ... end"
locs here refers to the ident's location, not whole pat *)
-type cases_pattern =
- | PatVar of Loc.t * Name.t
- | PatCstr of Loc.t * constructor * cases_pattern list * Name.t
+type cases_pattern_r =
+ | PatVar of Name.t
+ | PatCstr of constructor * cases_pattern list * Name.t
(** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
+and cases_pattern = cases_pattern_r Loc.located
(** Representation of an internalized (or in other words globalized) term. *)
type glob_constr =