diff options
| author | Emilio Jesus Gallego Arias | 2020-03-13 07:17:57 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:57 -0400 |
| commit | f759aaf9de94a11aa34a31c869829d60243d273d (patch) | |
| tree | 3934cdf4dada8bd15be3b8f39bae36e6e3ad519b /ide | |
| parent | ef3079e22fa7941d3335d7779c840e8d2d2bde39 (diff) | |
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 6 |
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 -> |
