]> matita.cs.unibo.it Git - helm.git/commitdiff
replaced fun with inverse attribute
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 14 Nov 2002 18:02:19 +0000 (18:02 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 14 Nov 2002 18:02:19 +0000 (18:02 +0000)
helm/gTopLevel/mQueryGenerator.ml

index 9f52c2f20a8f25661d1b6ba403bfdc5d1359c9e7..c05cba1c710c6f824d9b6c575f807e64ea2edb94 100644 (file)
@@ -185,7 +185,7 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "objectName" (M.Const [s])) in
+   let q = M.Ref (M.Attribute true M.ExactOp ["objectName"] (M.Const [s])) in
    execute_query q
 
 let backward e c t level =
@@ -193,7 +193,7 @@ 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.Relation (false, M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
                 M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
               )),      M.VVar "universe"
                       )
@@ -208,7 +208,7 @@ 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.Relation (false, M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
                 M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
                )
    in