diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-26 11:53:09 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-04 14:14:32 +0100 |
| commit | db65876404c7c3a1343623cc9b4d6c2a7164dd95 (patch) | |
| tree | 2f73652c1014775aa0fc171f9a64a8807ede7ac5 /intf/vernacexpr.mli | |
| parent | eef907ed0a200e912ab2eddc0fcea41b5f61c145 (diff) | |
Vernac classification: allow for commands which start proofs but must be synchrone.
The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index d1ed1d4ab..4f666a801 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -441,7 +441,7 @@ type vernac_type = | VtStm of vernac_control * vernac_part_of_script | VtUnknown and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * Id.t list +and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list and vernac_is_alias = bool and vernac_part_of_script = bool @@ -453,6 +453,9 @@ and vernac_control = | VtObserve of Stateid.t | VtBack of Stateid.t | VtPG +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) type vernac_when = | VtNow | VtLater |