ocaml 3.09 transition

[helm.git] / helm / mathql / query.xml

diff --git a/helm/mathql/query.xml b/helm/mathql/query.xml
index 68fb9992e42064a9de3f9489a9efc7c97bb34c6d..4efca730d4e72a6b8697adc2471fe174a785c673 100644 (file)
--- a/helm/mathql/query.xml
+++ b/helm/mathql/query.xml
@@ -1,29 +1,31 @@
 <?xml version="1.0" encoding="ISO-8859-1"?>
 
-<!DOCTYPE MathQL SYSTEM "xmathql.dtd">
+<!DOCTYPE MQLquery SYSTEM "xmathql.dtd">
 
-<!-- To validate: xmllint -valid -loaddtd -noout proquery.xml -->
+<!-- To validate: xmllint -valid -loaddtd -noout query.xml -->
 
-<MathQL>
+<MQLquery>
  <Select>
   <In>
-   <Use>
-    <Pattern arg="cic:/Coq/Init/Logic/Equality/eq.ind"/>
-    <Position binder="$1"/>
-   </Use>
+   <Relation name="Use">
+    <Pattern>
+     <CONST>cic:/Coq/Init/Logic/Equality/eq.ind</CONST>
+    </Pattern>
+    <Attr binder="$1"/>
+   </Relation>
   </In>
-  <Where rvar="result">
+  <Where rvar="@result">
    <AND>
-    <IS>
-     <BINDER name="$1"/>
-     <POSITION name="MainHypothesis"/>
-    </IS>
-    <IS>
-     <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
+    <EQ>
+     <BINDER name="$1"><Rvar name="@result"/></BINDER>
+     <CONST>MainHypothesis</CONST>
+    </EQ>
+    <EQ>
+     <PROPERTY name="TITLE"><REFOF><Rvar name="@result"/></REFOF></PROPERTY>
      <CONST>Uguaglianza</CONST>
-    </IS>
+    </EQ>
    </AND>
   </Where>
  </Select>
-</MathQL>
+</MQLquery>