aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc/deps/αβ/γδ.v
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-05 18:49:12 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-05 18:49:12 +0200
commit73620255a7a62703a89026336f97a4bc8a913afd (patch)
tree0b28d62d27b3fe6e94a07845ca8900cc9b3c9a71 /test-suite/misc/deps/αβ/γδ.v
parentf78a39499ef210456dd96ecb9896874c9ce300ae (diff)
parenta47a249e8c31dece9b816bc49d6c5a2aa50fb21b (diff)
Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 to escape non-UTF-8 file names)
Diffstat (limited to 'test-suite/misc/deps/αβ/γδ.v')
-rw-r--r--test-suite/misc/deps/αβ/γδ.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/misc/deps/αβ/γδ.v b/test-suite/misc/deps/αβ/γδ.v
new file mode 100644
index 000000000..f43a2d657
--- /dev/null
+++ b/test-suite/misc/deps/αβ/γδ.v
@@ -0,0 +1,4 @@
+Theorem simple : forall A, A -> A.
+Proof.
+auto.
+Qed.