X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=7dbf75262dd74bed7f4ab07f6b88d33d7a536e98;hb=14c77c97790562bd07405a290e3517c2532b7d12;hp=7ffe6e20837278403f11486d4f8740bc2d1a1b1f;hpb=27602e8f9a442b1effd75cd8f3e8b1f8a8a9d90d;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 7ffe6e208..7dbf75262 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -177,8 +177,8 @@ let backward e c t level =
    let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
    let q_where = M.Sub (M.RefOf (
       M.Select ("uri", 
-                M.Relation (M.ExactOp, "refObj", M.RVar "uri0", ["pos"]),
-                M.Ex (M.Meet (M.VVar "positions", M.Record ("uri", "pos")))
+                M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
+                M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
 	       )),      M.VVar "universe"
 		       )
    in
@@ -192,8 +192,8 @@ let backward e c t level =
    let build_select (r, b, v) =
       let pos = if b then "MainConclusion" else "InConclusion" in
       M.Select ("uri", 
-                M.Relation (M.ExactOp, "backPointer", M.Ref (M.Const [r]), ["pos"]),
-                M.Ex (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
+                M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
+                M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
                )
    in 
    let rec build_intersect = function