From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 25 Sep 2002 14:00:17 +0000 (+0000)
Subject: binders list specified in MathQL.Ex constructors
X-Git-Tag: new_mathql_before_first_merge~28
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=130b8e71a61cf5305894914c6f6431a9e924923c;p=helm.git

binders list specified in MathQL.Ex constructors
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 429d445f7..7dbf75262 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -178,7 +178,7 @@ let backward e c t level =
    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.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
 	       )),      M.VVar "universe"
 		       )
    in
@@ -193,7 +193,7 @@ let backward e c t level =
       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.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
                )
    in 
    let rec build_intersect = function