Better handling of queries. Now both the locate and backward queries give

[helm.git] / helm / gTopLevel / topLevel / topLevel.ml

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 9992e409369e8c33de911cc622840b8615c376a2..1fa790b64adc19e4614c402022d916dea9206d41 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -41,7 +41,7 @@ let pp_type_of uri =
 
 let locate name =
    check_db ();
-   print_endline (MQueryGenerator.locate_html name);
+   print_endline (snd (MQueryGenerator.locate name)) ;
    flush stdout
 
 let rec display = function
@@ -70,7 +70,7 @@ let mbackward n m l =
       | term :: tail -> 
          backward level tail;
          print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-         print_endline (MQueryGenerator.backward [] [] term level);
+         print_endline (snd (MQueryGenerator.backward [] [] term level)) ;
          flush stdout
    in
    check_db ();