X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2Fmathql.ml;h=e78029036f28f5dcb963d5d01564941fe399c2ff;hb=7f510b2df638258669d6539861a3f06ed5fab773;hp=01cbf431a21b5103963c9fa716b190f07405600f;hpb=9f45f8febfade5e1dca7a022154f2635be2af9b2;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mathql.ml b/helm/ocaml/mathql_interpreter/mathql.ml
index 01cbf431a..e78029036 100644
--- a/helm/ocaml/mathql_interpreter/mathql.ml
+++ b/helm/ocaml/mathql_interpreter/mathql.ml
@@ -93,6 +93,10 @@ type mqstring =
    | MQMConclusion                           (* main conclusion *)
    | MQConclusion                            (* inner conclusion *)
 
+type mqorder =
+   | MQAsc
+   | MQDesc
+
 type mqbool =
    | MQTrue
    | MQFalse
@@ -100,12 +104,13 @@ type mqbool =
    | MQOr of mqbool * mqbool
    | MQNot of mqbool
    | MQIs of mqstring * mqstring             (* operands *)
+   | MQSetEqual of mqlist * mqlist           (* the two lists denote the *)
+                                             (* same set                 *)
+   | MQSubset of mqlist * mqlist             (* the two lists denote two   *)
+                                             (* sets, the first one        *)
+                                             (* subsect of the second one. *)
 
-type mqorder =
-   | MQAsc
-   | MQDesc
-
-type mqlist =
+and mqlist =
    | MQSelect of mqrvar * mqlist * mqbool    (* rvar, list, boolean *) 
    | MQUse of mqlist * mqsvar                (* list, Position attribute *)
    | MQUsedBy of mqlist * mqsvar             (* list, Position attribute *)
@@ -114,6 +119,7 @@ type mqlist =
    | MQDiff of mqlist * mqlist               (*  *)
    | MQIntersect of mqlist * mqlist          (*  *)
    | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
+   | MQRVarOccur of mqrvar
 
 type mquery =
    | MQList of mqlist