From c5e6f5ee545ee24541836233a18c0c772077fbdf Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Wed, 8 Mar 2017 14:57:16 -0500
Subject: Run non-tactic comands without resilient_command

---
 stm/stm.ml                           | 11 +++++++----
 test-suite/output/ErrorInModule.out  |  2 ++
 test-suite/output/ErrorInModule.v    |  4 ++++
 test-suite/output/ErrorInSection.out |  2 ++
 test-suite/output/ErrorInSection.v   |  4 ++++
 5 files changed, 19 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/output/ErrorInModule.out
 create mode 100644 test-suite/output/ErrorInModule.v
 create mode 100644 test-suite/output/ErrorInSection.out
 create mode 100644 test-suite/output/ErrorInSection.v

diff --git a/stm/stm.ml b/stm/stm.ml
index f577994ffa..56243b76f9 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2136,10 +2136,13 @@ let known_state ?(redefine_qed=false) ~cache id =
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
-            resilient_command reach view.next;
-            vernac_interp id x;
-	    if eff then update_global_env ()
-          ), (if eff then `Yes else cache), true
+          (match !Flags.async_proofs_mode with
+           | Flags.APon | Flags.APonLazy ->
+             resilient_command reach view.next
+           | Flags.APoff -> reach view.next);
+          vernac_interp id x;
+          if eff then update_global_env ()
+        ), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             resilient_command reach view.next;
             vernac_interp id x;
diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
new file mode 100644
index 0000000000..851ecd9306
--- /dev/null
+++ b/test-suite/output/ErrorInModule.out
@@ -0,0 +1,2 @@
+File "stdin", line 3, characters 20-31:
+Error: The reference nonexistent was not found in the current environment.
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
new file mode 100644
index 0000000000..e69e23276b
--- /dev/null
+++ b/test-suite/output/ErrorInModule.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+Module M.
+  Definition foo := nonexistent.
+End M.
diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out
new file mode 100644
index 0000000000..851ecd9306
--- /dev/null
+++ b/test-suite/output/ErrorInSection.out
@@ -0,0 +1,2 @@
+File "stdin", line 3, characters 20-31:
+Error: The reference nonexistent was not found in the current environment.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
new file mode 100644
index 0000000000..3036f8f05b
--- /dev/null
+++ b/test-suite/output/ErrorInSection.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+Section S.
+  Definition foo := nonexistent.
+End S.
-- 
cgit v1.2.3