diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-14 06:57:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:23:40 +0100 |
| commit | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (patch) | |
| tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /stm/stm.mli | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
[located] More work towards using CAst.t
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
Diffstat (limited to 'stm/stm.mli')
| -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 f967c9815..a8eb10fb3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -80,7 +80,7 @@ val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> - Vernacexpr.vernac_control Loc.located + Vernacexpr.vernac_control CAst.t (* Reminder: A parsable [pa] is constructed using [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) @@ -94,7 +94,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_control Loc.located -> + bool -> Vernacexpr.vernac_control CAst.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], |