diff options
| author | Maxime Dénès | 2017-10-20 11:03:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-20 11:03:09 +0200 |
| commit | 8492fa8d2aa0e77b7c571956ee21097977b1df15 (patch) | |
| tree | 1ac1bd71bb93cef862f4527f0a31923cb5b03cb7 /toplevel | |
| parent | 09525d09e414d3582595ffd141702e69a9a2efb9 (diff) | |
| parent | 286d387082fb0f86858dce661c789bdcb802c295 (diff) | |
Merge PR #1095: [stm] Remove state handling from Futures
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d736975d32..cf63fbdc3d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -119,7 +119,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) = (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the - document. Hopefully this is fixed when VtBack can be removed + document. Hopefully this is fixed when VtMeta can be removed and Undo etc... are just interpreted regularly. *) (* XXX: The classifier can emit warnings so we need to guard @@ -127,7 +127,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) = let wflags = CWarnings.get_flags () in CWarnings.set_flags "none"; let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with - | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true + | VtProofStep _ | VtMeta | VtStartProof _ -> true | _ -> false in CWarnings.set_flags wflags; |