aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-02-18 17:27:39 +0100
committerPierre-Marie Pédrot2015-02-18 17:27:39 +0100
commit4bb062f4a66c4ae5a1742e7d99fdc335de0d57a9 (patch)
treeaf8ead1cdc5af3842e683f602177ab4fa2dec9b5 /test-suite/output
parent1be9c4da4d814c29d4ba45b121fda924adc1130e (diff)
parent29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/simpl.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index 89638eedd7..5f1926f142 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x.
intro x.
simpl (_ + x).
Show.
-Undo 2.
+Undo.
simpl (_ + x) at 2.
Show.
-Undo 2.
+Undo.
simpl (0 + _).
Show.
-Undo 2.
+Undo.