From 84accdaea3ce094cc5d0232107d3e2ea654a76c2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Mon, 18 Sep 2017 13:27:20 +0200
Subject: Remove STM vernaculars.

---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1602f9c68..22dc02f03 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -134,7 +134,7 @@ let rec interp_vernac sid (loc,com) =
          document. Hopefully this is fixed when VtBack can be removed
          and Undo etc... are just interpreted regularly. *)
       let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
-        | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+        | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
         | _ -> false
       in
 
-- 
cgit v1.2.3