From 209ff6ae4367b8c96b59bc318f4791dcb2251c14 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 23 Mar 2017 15:11:46 -0400
Subject: Correctly identify [Time Defined.] as a defined

Need to check inside control expressions. Also fixes handling of
[Redirect "file" Defined.] and [Timeout n Defined.].

Fixes Coq bug 5411 (https://coq.inria.fr/bugs/show_bug.cgi?id=5411):
coqc -quick hangs on [Time Defined.]
---
 stm/stm.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index f577994ffa..71ec8acc68 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1912,10 +1912,14 @@ let collect_proof keep cur hd brkind id =
    | [] -> no_name
    | id :: _ -> Id.to_string id in
  let loc = (snd cur).loc in
- let is_defined = function
-   | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
-      true
+ let rec is_defined_expr = function
+   | VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) -> true
+   | VernacTime (_, e) -> is_defined_expr e
+   | VernacRedirect (_, (_, e)) -> is_defined_expr e
+   | VernacTimeout (_, e) -> is_defined_expr e
    | _ -> false in
+ let is_defined = function
+   | _, { expr = e } -> is_defined_expr e in
  let proof_using_ast = function
    | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
    | _ -> None in
-- 
cgit v1.2.3


From 48c44b55b76e75aa2af9f82753c6ffe7531790c8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 5 Apr 2017 18:18:56 +0200
Subject: Fix a few programming pearls related to Time, Fail and Redirect.

This fixes a few clear bugs, but the STM code handling Time, Fail and
Redirect before par: still needs to be rewritten. It does not implement
the same semantics as the vernac interpreter for Fail Fail [c] and
ignores Redirect.

This commit was already reviewed with Enrico and tested on Travis.
---
 stm/stm.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 56243b76f9..3efad70fb2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1746,12 +1746,13 @@ end = struct (* {{{ *)
     { indentation; verbose; loc; expr = e; strlen }
   =
     let e, time, fail =
-      let rec find time fail = function
-        | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
-        | VernacFail e -> find time true e
-        | _ -> e, time, fail in find false false e in
+      let rec find ~time ~fail = function
+        | VernacTime (_,e) -> find ~time:true ~fail e
+        | VernacRedirect (_,(_,e)) -> find ~time ~fail e
+        | VernacFail e -> find ~time ~fail:true e
+        | e -> e, time, fail in find ~time:false ~fail:false e in
     Hooks.call Hooks.with_fail fail (fun () ->
-    (if time then System.with_time false else (fun x -> x)) (fun () ->
+    (if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
       let goals, _, _, _, _ = Proof.proof p in
-- 
cgit v1.2.3


From e73b124a9d504e1759d4a4a0d3899882f58d459a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 16:12:58 +0200
Subject: Fix anomaly when doing [all:Check _.] during a proof.

---
 stm/vernac_classifier.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index dc5be08a37..58a86a4aa5 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -219,8 +219,8 @@ let rec classify_vernac e =
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
-    | VernacWriteState _ -> VtUnknown, VtNow
-    | VernacError _ -> assert false
+    | VernacWriteState _
+    | VernacError _ -> VtUnknown, VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
-- 
cgit v1.2.3