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 /stm | |
| parent | ef3079e22fa7941d3335d7779c840e8d2d2bde39 (diff) | |
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 88da3c747f..2c27d63b82 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -93,7 +93,7 @@ val new_doc : stm_init_options -> doc * Stateid.t be the case if an error was raised at parsing time). *) val parse_sentence : doc:doc -> Stateid.t -> - entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.G.Parsable.t -> 'a + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a (* Reminder: A parsable [pa] is constructed using [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) @@ -119,7 +119,7 @@ val get_proof : doc:doc -> Stateid.t -> Proof.t option throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : doc:doc -> - at:Stateid.t -> route:Feedback.route_id -> Pcoq.G.Parsable.t -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following |