aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-13 07:17:57 -0400
committerEmilio Jesus Gallego Arias2020-03-25 23:45:57 -0400
commitf759aaf9de94a11aa34a31c869829d60243d273d (patch)
tree3934cdf4dada8bd15be3b8f39bae36e6e3ad519b /plugins/ssr
parentef3079e22fa7941d3335d7779c840e8d2d2bde39 (diff)
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrparser.mlg22
1 files changed, 11 insertions, 11 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index c3396584a4..442b40221b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -263,16 +263,16 @@ let negate_parser f tok x =
| Some _ -> raise Stream.Failure
let test_not_ssrslashnum =
- Pcoq.G.Entry.of_parser
+ Pcoq.Entry.of_parser
"test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
let test_ssrslashnum00 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+ Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
let test_ssrslashnum10 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+ Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
let test_ssrslashnum11 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+ Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
let test_ssrslashnum01 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+ Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
}
@@ -459,7 +459,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "@" -> xWithAt
| _ -> xNoFlag
-let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
(* New kinds of terms *)
@@ -470,7 +470,7 @@ let input_term_annotation _ strm =
| Tok.KEYWORD "@" :: _ -> `At
| _ -> `None
let term_annotation =
- Pcoq.G.Entry.of_parser "term_annotation" input_term_annotation
+ Pcoq.Entry.of_parser "term_annotation" input_term_annotation
(* terms *)
@@ -811,7 +811,7 @@ let reject_ssrhid _ strm =
| _ -> ())
| _ -> ()
-let test_nohidden = Pcoq.G.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
let rec reject_binder crossed_paren k tok s =
match
@@ -825,7 +825,7 @@ let rec reject_binder crossed_paren k tok s =
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
| _ -> if crossed_paren then () else raise Stream.Failure
-let _test_nobinder = Pcoq.G.Entry.of_parser "test_nobinder" (reject_binder false 0)
+let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0)
}
@@ -1659,7 +1659,7 @@ let ssr_id_of_string loc s =
^ "Scripts with explicit references to anonymous variables are fragile."))
end; Id.of_string s
-let ssr_null_entry = Pcoq.G.Entry.of_parser "ssr_null" (fun _ _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
}
@@ -2382,7 +2382,7 @@ let test_ssr_rw_syntax =
match Util.stream_nth 0 strm with
| Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
| _ -> raise Stream.Failure in
- Pcoq.G.Entry.of_parser "test_ssr_rw_syntax" test
+ Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
}