diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 12:20:00 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:01 -0400 |
| commit | af7628468d638c77fb3f55a9eb315b687b76a21d (patch) | |
| tree | 63cfb1a71815b956d5a79cf83b4d5284626d1d1e /stm | |
| parent | f9174f64c56375adb42e53b97df9eeb8b0a9680d (diff) | |
[parsing] Remove redundant interfaces from Pcoq
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
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 2c27d63b82..88da3c747f 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.Parsable.t -> 'a + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.G.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.Parsable.t -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.G.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 |