]> matita.cs.unibo.it Git - helm.git/commitdiff
generator patched
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 27 Nov 2002 10:42:22 +0000 (10:42 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 27 Nov 2002 10:42:22 +0000 (10:42 +0000)
helm/gTopLevel/mQueryGenerator.ml

index b12f19bace500030c256e89d0090dab59a267090..75c23e837dc5f929c456ce4c767eec90380b0ac6 100644 (file)
@@ -108,7 +108,8 @@ let searchPattern e c t level =
        (M.Select
          ("uri", 
            M.Relation
-            (false, M.RefineExact, in_path "refObj", M.RVar "uri0", 
+            (false, M.RefineExact, in_path "refObj", 
+            M.Ref (M.RefOf (M.RVar "uri0")), 
             [assign "pos" "position"]),
            M.Ex ["uri"]
             (M.Meet (M.VVar "positions", M.Record ("uri", in_path "pos")))