experimental/ulo: explain problems with data properties

experimental/ulo/coq-export-bugs.txt

-- tags that shouldn't be there, i.e. `Target`, `HasInHypothesis` and
-  so on
+The Coqxml [1] exports have some bugs.
 
-- wrong ULO namespace
+* The RDF files contain tags that should not be there. For example,
+  `<Target>`, `<HasInHypothesis>` and so on.
 
-- objects have relative URIs which is annoying; this might be annoying
-  but it is not a bug
+* The ULO namespace is wrong. It should be
+
+    https://mathhub.info/ulo#
+
+  as defined in the ontology file [2].
+
+* Handling of data properties seems wrong. Data properties are
+
+    `ulo:sourceref`, `ulo:docref` and `ulo:internal-size`
+
+  as well as some imported dcterms, that is
+
+    `dcterms:title` and `dcterms:isVersionOf`
+
+  In the Coqxml exports, these are used together with references,
+  e.g.
+
+    <ulo:docref rdf:resource="Coq.Arith.Between.html#bet_eq" />
+    <ulo:sourceref rdf:resource="32" />
+
+  but RDF/XML requires the rdf:resource to be an IRI. Here, this is
+  not the case. A standard-compliant example of the code above should
+  like like this
+
+    <ulo:docref>Coq.Arith.Between.html#bet_eq</ulo:docref>
+    <ulo:sourceref>32</ulo:sourceref>
+
+  which makes the values literals.
+
+[1] https://gl.mathhub.info/Coqxml
+[2] https://gl.mathhub.info/ulo/ulo/-/blob/master/ulo.owl