From 130b8e71a61cf5305894914c6f6431a9e924923c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 Sep 2002 14:00:17 +0000 Subject: [PATCH] binders list specified in MathQL.Ex constructors --- helm/gTopLevel/mQueryGenerator.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2