aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/replace.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/replace.v')
-rw-r--r--test-suite/success/replace.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v
index 94b75c7f0..6acdd5161 100644
--- a/test-suite/success/replace.v
+++ b/test-suite/success/replace.v
@@ -5,7 +5,7 @@ Undo.
intros x H H0.
replace x with 0.
Undo.
-replace x with 0 in |- *.
+replace x with 0 in |- *.
Undo.
replace x with 1 in *.
Undo.