aboutsummaryrefslogtreecommitdiff
path: root/ide
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 /ide
parentef3079e22fa7941d3335d7779c840e8d2d2bde39 (diff)
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Diffstat (limited to 'ide')
-rw-r--r--ide/idetop.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 81e7e4d148..0ef7fca41f 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -91,7 +91,7 @@ let set_doc doc = ide_doc := Some doc
let add ((s,eid),(sid,verbose)) =
let doc = get_doc () in
- let pa = Pcoq.G.Parsable.make (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
| None -> assert false (* s is not an empty string *)
| Some ast ->
@@ -127,13 +127,13 @@ let edit_at id =
* be removed in the next version of the protocol.
*)
let query (route, (s,id)) =
- let pa = Pcoq.G.Parsable.make (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let doc = get_doc () in
Stm.query ~at:id ~doc ~route pa
let annotate phrase =
let doc = get_doc () in
- let pa = Pcoq.G.Parsable.make (Stream.of_string phrase) in
+ let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
| None -> Richpp.richpp_of_pp 78 (Pp.mt ())
| Some ast ->