From: Ferruccio Guidi Date: Thu, 14 Nov 2002 18:02:19 +0000 (+0000) Subject: replaced fun with inverse attribute X-Git-Tag: V_0_0_3~10 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f0843578d190c26c6975502a33dd01ca1c4aa8eb replaced fun with inverse attribute --- diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index 9f52c2f20..c05cba1c7 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.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