let term = disambiguate term status in
let uri =
match term with
- | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n])
+ | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
| _ -> failwith "Not a MutInd"
in
let l = MQ.elim ~dbd uri in
(TA.Executable (loc,
(TA.Tactical (loc,
TA.Tactic (loc,
- TA.Apply (loc, CicAst.Uri (uri,None)))))))
+ TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))))
in
let new_status = MatitaEngine.eval_ast status ast in
let extra_text =
MatitaLog.error
"The result of the urichooser should be only 1 uri, not:\n";
List.iter (
- fun u -> MatitaLog.error (u ^ "\n")
+ fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
) selected;
assert false)
| TA.Check (_,term) ->