summaryrefslogtreecommitdiff
path: root/test-suite/output/Remark2.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Remark2.v')
-rw-r--r--test-suite/output/Remark2.v8
1 files changed, 0 insertions, 8 deletions
diff --git a/test-suite/output/Remark2.v b/test-suite/output/Remark2.v
deleted file mode 100644
index e1ef57a0..00000000
--- a/test-suite/output/Remark2.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Section A.
-Section B.
-Section C.
-Remark t : True. Proof I.
-End C.
-End B.
-End A.
-Locate B.C.t.