]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed references to functions moved from Misc to MQueryMisc
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 20 Feb 2003 17:16:13 +0000 (17:16 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 20 Feb 2003 17:16:13 +0000 (17:16 +0000)
helm/gTopLevel/disambiguate.ml

index 2f02818474b5ccdd1e2f606dd0470817e85c2571..c0e1818e1d18532c6fe480c6f00d05e81112b463 100644 (file)
@@ -75,7 +75,7 @@ module Make(C:Callbacks) =
     let uris =
      List.map
       (function uri,_ ->
-        Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+        MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
     let html=
      " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
@@ -100,7 +100,7 @@ module Make(C:Callbacks) =
           ~id
           uris
      in
-      List.map Misc.cic_textual_parser_uri_of_string uris'
+      List.map MQueryMisc.cic_textual_parser_uri_of_string uris'
 
 
    exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput