X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=78ce04e6c81c500fbdacab9a9b9f106cbd35d433;hb=3d828e15aa6d919eee55f8aa803f3512991e6693;hp=c05cba1c710c6f824d9b6c575f807e64ea2edb94;hpb=f0843578d190c26c6975502a33dd01ca1c4aa8eb;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index c05cba1c7..78ce04e6c 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -185,7 +185,7 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Attribute true M.ExactOp ["objectName"] (M.Const [s])) in
+   let q = M.Ref (M.Attribute true M.RefineExact ("objectName", []) (M.Const [s])) in
    execute_query q
 
 let backward e c t level =
@@ -193,8 +193,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 (false, M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
-                M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
+                M.Relation (false, M.RefineExact, ("refObj", []), M.RVar "uri0", ["pos"]),
+                M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", ("pos", [])))) 
 	       )),      M.VVar "universe"
 		       )
    in
@@ -208,8 +208,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 (false, M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
-                M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
+                M.Relation (false, M.RefineExact, ("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