X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fquery.xml;h=4efca730d4e72a6b8697adc2471fe174a785c673;hb=6e7fd1727eafb8280d2a01c05eddf49d19db2aaa;hp=e51944e8d49cd802949a73ad2009f503a0ab088c;hpb=85f01e5719399cc2ccf47cbe51f7b8036e12d815;p=helm.git

diff --git a/helm/mathql/query.xml b/helm/mathql/query.xml
index e51944e8d..4efca730d 100644
--- a/helm/mathql/query.xml
+++ b/helm/mathql/query.xml
@@ -7,36 +7,23 @@
 <MQLquery>
  <Select>
   <In>
-   <Use>
+   <Relation name="Use">
     <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>
+     <CONST>cic:/Coq/Init/Logic/Equality/eq.ind</CONST>
     </Pattern>
-    <Position binder="$1"/>
-   </Use>
+    <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>