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.]

1 files changed, 7 insertions, 3 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index f577994ff..71ec8acc6 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