]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fwdSimplTactic.ml
many strings that are supposed to be URIs are now UriManager.uri
[helm.git] / helm / ocaml / tactics / fwdSimplTactic.ml
index c1a5347f42d034a157a7e7aec3852b631a0a031f..7981ac8753727962ad64f8443c13385a642b6e77 100644 (file)
@@ -82,6 +82,6 @@ let fwd_simpl_tac ~hyp ~dbd =
       let major = declaration hyp context in 
       match  MetadataQuery.fwd_simpl ~dbd major with
          | []       -> error fail_msg1
-         | uri :: _ -> prerr_endline uri; (proof, [])  
+         | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])  
    in
    PET.mk_tactic fwd_simpl_tac