From df8717e9b0141ba91a0eb480ba10c07a108a080e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Tue, 16 Jun 2020 10:09:45 +0200
Subject: [PATCH] note down bugs in the Coq export

---
 experimental/ulo/coq-export-bugs.txt | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 experimental/ulo/coq-export-bugs.txt

diff --git a/experimental/ulo/coq-export-bugs.txt b/experimental/ulo/coq-export-bugs.txt
new file mode 100644
index 0000000..1839692
--- /dev/null
+++ b/experimental/ulo/coq-export-bugs.txt
@@ -0,0 +1,6 @@
+- tags that shouldn't be there, i.e. `Target`, `HasInHypothesis` and
+  so on
+
+- wrong ULO namespace
+
+- objects have relative URIs which is annoying
-- 
GitLab