]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
MQueryUtil updated
[helm.git] / helm / ocaml / mathql / mathQL.ml
index 088d598a4562a260c6c039d5ca097c3ba2de5af2..d102e730100deab17fca3672e92a0ac2b3f3a5ba 100644 (file)
@@ -91,8 +91,8 @@ type mqfunc =
 type mqstring =
    | MQCons of string                       (* constant *)
    | MQFunc of mqfunc * mqrvar              (* function, rvar *)
-   | MQRVar of mqrvar                       (* rvar *)
-   | MQSVar of mqsvar                       (* svar *)
+   | MQSRVar of mqrvar                      (* rvar *)
+   | MQSSVar of mqsvar                      (* svar *)
    | MQMConclusion                          (* main conclusion *)
    | MQConclusion                           (* inner conclusion *)
 
@@ -121,7 +121,7 @@ and mqlist =
    | MQUnion of mqlist * mqlist             (* operands                   *)
    | MQIntersect of mqlist * mqlist         (* operands                   *)
    | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
-   | MQRVarOccur of mqrvar
+   | MQLRVar of mqrvar
    | MQDiff of mqlist * mqlist               (*  *)
 
 type mquery =