aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-26 19:34:14 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-27 11:27:35 +0100
commit7d0eb42050cb4f75c95cefb11c0cac5efa32f40a (patch)
tree324e9f9ffc52187df47c144d110204c090e02f19 /parsing
parent257e14b19e9026a4f3cdfa991e27293faf110324 (diff)
A cosmetic standardization: adding a space in g_constr.ml4.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6af8f0b9e..7e5933cea 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -391,7 +391,7 @@ GEXTEND Gram
| _ -> CErrors.user_err
?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
(Pp.str "Such pattern cannot have arguments."))
- |"@"; r = Prim.reference; lp = LIST0 NEXT ->
+ | "@"; r = Prim.reference; lp = LIST0 NEXT ->
CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
| "1" LEFTA
[ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ]