]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/metadataQuery.ml
lapply and fwd improved
[helm.git] / helm / ocaml / tactics / metadataQuery.ml
index a3e774d1d84e46f7345392f81780cc212d229732..a01044e8cf15ecc5f8434bec7faa26be5b0d52fe 100644 (file)
@@ -500,8 +500,8 @@ let get_metadata t =
 let debug_metadata = function
    | None                 -> ()
    | Some (outer, inners) -> 
-      let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n uri in
-      Printf.eprintf "\n%s: %s\n" "fwd" outer;
+      let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in
+      Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer);
       List.iter f inners; prerr_newline ()
 
 let fwd_simpl ~dbd t =
@@ -525,8 +525,9 @@ let fwd_simpl ~dbd t =
    let compare (_, x) (_, y) = compare x y in
    let filter n (uri, rank) =
       if rank > 0 then Some (UriManager.uri_of_string uri) else None
-   in   
-   match get_metadata t with
+   in
+   let metadata = get_metadata t in debug_metadata metadata;
+   match metadata with
       | None                 -> []
       | Some (outer, inners) ->
          let select = "source, h_inner, h_index" in
@@ -539,4 +540,4 @@ let fwd_simpl ~dbd t =
          let lemmas = Mysql.map result ~f:(map inners) in
         let ranked = List.fold_left rank [] lemmas in
         let ordered = List.rev (List.fast_sort compare ranked) in
-        map_filter filter 0 ordered
+         map_filter filter 0 ordered