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