X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fmquery.ml;h=093f0228cfc7b7696010b6610b4305808838f435;hb=528294d5228f65f4b3fbd3ebe00a5cd9a8f3b929;hp=2812bd64e02f352c824c17d0bb3eb8260f594bbe;hpb=d7e5adc6adcdcbc98964fa73b3d8e05cad428a6b;p=helm.git

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 2812bd64e..093f0228c 100644
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -72,8 +72,8 @@ let out_func = function
 
 let out_str = function
    | MQCons s      -> con s
-   | MQRVar s      -> out_rvar s
-   | MQSVar s      -> out_svar s
+   | MQSRVar s      -> out_rvar s
+   | MQSSVar s      -> out_svar s
    | MQFunc (f, r) -> out_func f ^ out_rvar r
    | MQMConclusion -> key "mainconclusion" 
    | MQConclusion  -> key "conclusion" 
@@ -98,7 +98,7 @@ and out_list = function
    | MQPattern p -> key "pattern" ^ out_pat p
    | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
    | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
-   | MQRVarOccur v -> key "rvaroccur" ^ v
+   | MQLRVar v -> key "rvaroccur" ^ v
 
 let out_query = function
    | MQList l -> out_list l
@@ -244,7 +244,7 @@ let build_select (r, b, v) n =
    let mqs = if b then MQMConclusion else MQConclusion in
    MQSelect (rvar, 
              MQUse (MQPattern r, svar),
-             MQIs (MQSVar svar, mqs)
+             MQIs (MQSSVar svar, mqs)
             )
 
 let rec build_inter n = function
@@ -274,10 +274,10 @@ let restrict_universe query =
         MQSubset (
          MQSelect (
           "uri2",
-          MQUsedBy (MQRVarOccur "uri", "pos"),
+          MQUsedBy (MQLRVar "uri", "pos"),
           MQOr (
-           MQIs (MQSVar "pos", MQConclusion),
-           MQIs (MQSVar "pos", MQMConclusion)
+           MQIs (MQSSVar "pos", MQConclusion),
+           MQIs (MQSSVar "pos", MQMConclusion)
           )
          ),
          universe