]> matita.cs.unibo.it Git - helm.git/commitdiff
generator patched
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 17 Oct 2002 15:02:52 +0000 (15:02 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 17 Oct 2002 15:02:52 +0000 (15:02 +0000)
helm/gTopLevel/mQueryGenerator.ml

index 6a1eb923d2eb6b50b3113d8c01d2192427b66eaa..4deaf8c7a23d8923828a75977f35c9a36b394b31 100644 (file)
@@ -185,7 +185,7 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "uri_of_alias" (M.Const [s])) in
+   let q = M.Ref (M.Fun "reference" (M.Const [s])) in
    execute_query q
 
 let backward e c t level =