diff options
| author | Enrico Tassi | 2019-06-13 17:40:05 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-13 17:40:05 +0200 |
| commit | 2e13fffea256312cd42a1bea221ae24ffda0fa28 (patch) | |
| tree | 0348b629d26571350822f8f69b02fb12d4948994 /vernac | |
| parent | 6132579961e33bb2c5eb05cf2c10096081a888c7 (diff) | |
| parent | 2e371e35b420e2f86f83cdac8b7a2c1816c40ef9 (diff) | |
Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLater
Ack-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacextend.ml | 19 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 13 |
2 files changed, 15 insertions, 17 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 6a52177dd5..c7008c2a84 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -16,7 +16,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop -type vernac_type = +type vernac_when = + | VtNow + | VtLater + +type vernac_classification = (* Start of a proof *) | VtStartProof of vernac_start (* Command altering the global state, bad for parallel @@ -37,7 +41,7 @@ type vernac_type = (* To be removed *) | VtMeta and vernac_start = opacity_guarantee * Names.Id.t list -and vernac_sideff_type = Names.Id.t list +and vernac_sideff_type = Names.Id.t list * vernac_when and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) @@ -48,11 +52,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *) and proof_block_name = string (** open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when - type typed_vernac = | VtDefault of (unit -> unit) @@ -130,9 +129,9 @@ let get_vernac_classifier (name, i) args = let declare_vernac_classifier name f = classifiers := String.Map.add name f !classifiers -let classify_as_query = VtQuery, VtLater -let classify_as_sideeff = VtSideff [], VtLater -let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater +let classify_as_query = VtQuery +let classify_as_sideeff = VtSideff ([], VtLater) +let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None} type (_, _) ty_sig = | TyNil : (vernac_command, vernac_classification) ty_sig diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 78b7f21b0d..fd59d77237 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -32,7 +32,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop -type vernac_type = +type vernac_when = + | VtNow + | VtLater + +type vernac_classification = (* Start of a proof *) | VtStartProof of vernac_start (* Command altering the global state, bad for parallel @@ -53,7 +57,7 @@ type vernac_type = (* To be removed *) | VtMeta and vernac_start = opacity_guarantee * Names.Id.t list -and vernac_sideff_type = Names.Id.t list +and vernac_sideff_type = Names.Id.t list * vernac_when and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) @@ -64,11 +68,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *) and proof_block_name = string (** open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when - (** Interpretation of extended vernac phrases. *) type typed_vernac = |