aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ide/coqide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2b07ca4c9f..f17beb6044 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1237,7 +1237,7 @@ Please restart and report NOW.";
self#clear_message
in
begin match last_command with
- | {ast=_,VernacSolve _} ->
+ | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} ->
begin
try Pfedit.undo 1; ignore (pop ()); update_input ()
with _ -> self#backtrack_to_no_lock start