X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fquery.xml;h=e51944e8d49cd802949a73ad2009f503a0ab088c;hb=b89599c60d93bfc05dc15d6e22348fcc87fa722f;hp=68fb9992e42064a9de3f9489a9efc7c97bb34c6d;hpb=c534f0f12f9369670d93dd0eb30e8f9a85ff6498;p=helm.git

diff --git a/helm/mathql/query.xml b/helm/mathql/query.xml
index 68fb9992e..e51944e8d 100644
--- a/helm/mathql/query.xml
+++ b/helm/mathql/query.xml
@@ -1,14 +1,29 @@
 <?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"/>
+    <Pattern>
+     <PPrefix><CONST>cic</CONST></PPrefix>
+     <PBody>
+      <SLASH/>
+      <CONST>Coq</CONST>
+      <SLASH/>
+      <CONST>Init</CONST>
+      <SLASH/>
+      <CONST>Logic</CONST>
+      <SLASH/>
+      <CONST>Equality</CONST>
+      <SLASH/>
+      <CONST>eq</CONST>
+     </PBody>
+     <Ext><CONST>ind</CONST></Ext>
+    </Pattern>
     <Position binder="$1"/>
    </Use>
   </In>
@@ -25,5 +40,5 @@
    </AND>
   </Where>
  </Select>
-</MathQL>
+</MQLquery>