Modified Files:

1) query.xml xmathql.dtd: pattern changed

diff --git a/helm/mathql/query.xml b/helm/mathql/query.xml
index 1910c00c05c28192d98df1cfc18fcf6f880e4fad..aff80bcb58b96020ddff6038f835fea852ab5cd7 100644 (file)
--- a/helm/mathql/query.xml
+++ b/helm/mathql/query.xml
@@ -9,7 +9,7 @@
   <In>
    <Use>
     <Pattern>
-     <Prefix>cic</Prefix>
+     <Prefix><CONST>cic</CONST></Prefix>
      <TokenList>
       <SLASH/>
       <CONST>Coq</CONST>

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index e32b0299fb7dbe57b8a7289fb0de99288cc6273e..a5bd242e7b108bd98d09e8386aba45db3527edcf 100644 (file)
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -152,10 +152,10 @@
 <!-- QUESTIONMARK matches one character except "/"                         --> 
 <!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
 
-<!ELEMENT Prefix (#PCDATA)>
+<!ELEMENT Prefix (CONST|STAR)>
 
 <!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
-<!ELEMENT FragmentID ((NUMBER|STAR), (NUMBER|STAR)?)>
+<!ELEMENT FragmentID (NUMBER|TWOSTARS|STAR)+>
 
 <!-- MathQL boolean expressions -->