]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/mQueryGenerator.ml
MQueryGenerator ported to use fun "objectName"
[helm.git] / helm / gTopLevel / mQueryGenerator.ml
index 4deaf8c7a23d8923828a75977f35c9a36b394b31..9f52c2f20a8f25661d1b6ba403bfdc5d1359c9e7 100644 (file)
@@ -185,7 +185,7 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "reference" (M.Const [s])) in
+   let q = M.Ref (M.Fun "objectName" (M.Const [s])) in
    execute_query q
 
 let backward e c t level =