aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 38355956cf..399205189b 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1304,7 +1304,7 @@ let known_state ?(redefine_qed=false) ~cache id =
let view = VCS.visit id in
match view.step with
| `Alias id -> (fun () ->
- reach view.next; reach id; Vernacentries.try_print_subgoals ()
+ reach view.next; reach id
), cache
| `Cmd (x,_) -> (fun () ->
reach view.next; vernac_interp id x