aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-09 03:35:20 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:33:36 +0200
commitee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch)
tree3b40c06375a463625a2675b90e009fcb0b64a7d2 /parsing
parent054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff)
[location] [ast] Port module AST to CAst
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml410
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 27f879154..7239bc23b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -511,11 +511,11 @@ GEXTEND Gram
(* Module expressions *)
module_expr:
[ [ me = module_expr_atom -> me
- | me1 = module_expr; me2 = module_expr_atom -> Loc.tag ~loc:!@loc @@ CMapply (me1,me2)
+ | me1 = module_expr; me2 = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (me1,me2)
] ]
;
module_expr_atom:
- [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
[ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
@@ -525,12 +525,12 @@ GEXTEND Gram
] ]
;
module_type:
- [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid)
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid)
| "("; mt = module_type; ")" -> mt
| mty = module_type; me = module_expr_atom ->
- Loc.tag ~loc:!@loc @@ CMapply (mty,me)
+ CAst.make ~loc:!@loc @@ CMapply (mty,me)
| mty = module_type; "with"; decl = with_declaration ->
- Loc.tag ~loc:!@loc @@ CMwith (mty,decl)
+ CAst.make ~loc:!@loc @@ CMwith (mty,decl)
] ]
;
(* Proof using *)