diff options
| author | Enrico Tassi | 2017-04-17 10:31:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-24 17:10:25 +0100 |
| commit | e43c35ba795520fe111ac39a834f334753491b28 (patch) | |
| tree | 751a2612627f5b5d4104a5269630e373d66db107 /vernac/vernacextend.ml | |
| parent | 9f347ed90495bcde875a5c3646f2291834118a84 (diff) | |
[STM] explicit handling of parsing states
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 05687afd8b..f5cf3401d0 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -29,15 +29,15 @@ type vernac_type = parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } - (* To be removed *) - | VtProofMode of string (* Queries are commands assumed to be "pure", that is to say, they don't modify the interpretation state. *) | VtQuery + (* Commands that change the current proof mode *) + | VtProofMode of string (* To be removed *) | VtMeta | VtUnknown -and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) |