diff options
| author | Enrico Tassi | 2014-09-08 13:17:06 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-09 13:11:38 +0200 |
| commit | 9d443eb0ff815a804f771335f0ac38a94d2851f2 (patch) | |
| tree | 3e98143409529e20f61169ea7dc1039376139a8b /intf/vernacexpr.mli | |
| parent | de5ed8e17df8433d4f0ffe6a6440505b5a530638 (diff) | |
Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 37048005fa..5bf83e2c19 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -453,7 +453,7 @@ type vernac_type = | VtStm of vernac_control * vernac_part_of_script | VtUnknown and report_with = Stateid.t (* report feedback on a different id *) -and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *) +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list and vernac_is_alias = bool |