aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coq.ml2
-rw-r--r--test-suite/ide/undo.v4
2 files changed, 3 insertions, 3 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index ac978e4cf..4c5179edd 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -461,7 +461,7 @@ struct
List.iter
(fun cmd ->
let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
- Vernac.eval_ctrl (snd (Vernac.parse_sentence (parsable_of_string str,None))))
+ Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string str,None)))
opt
let enforce_hack () = Hashtbl.iter set state_hack
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
index d5e9ee5e8..84eacc3e3 100644
--- a/test-suite/ide/undo.v
+++ b/test-suite/ide/undo.v
@@ -3,8 +3,8 @@
(* Undoing arbitrary commands, as first step *)
-Theorem a : O=O.
-Ltac f x := x.
+Theorem a : O=O. (* 2 *)
+Ltac f x := x. (* 1 * 3 *)
assert True by trivial.
trivial.
Qed.