]> matita.cs.unibo.it Git - helm.git/commitdiff
Generator updated for the new semantics of Relation
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 21 Sep 2002 18:37:43 +0000 (18:37 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 21 Sep 2002 18:37:43 +0000 (18:37 +0000)
helm/gTopLevel/mQueryGenerator.ml

index 7ffe6e20837278403f11486d4f8740bc2d1a1b1f..429d445f7ced89fbd8af701f9159c22fc419cecf 100644 (file)
@@ -177,7 +177,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 (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
                 M.Ex (M.Meet (M.VVar "positions", M.Record ("uri", "pos")))
               )),      M.VVar "universe"
                       )
@@ -192,7 +192,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 (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
                 M.Ex (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
                )
    in