Much simpler (and slightly more performant) implementation of the UriManager.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c7859a7c7b96df61e8501b289d146237bc0b5709..1f8add6a07b542c93823f1769393ef12590f3f5d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -169,7 +169,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
       let term = disambiguate term status in
       let uri =
         match term with
-        | Cic.MutInd (uri,n,_) -> UriManager.uri_of_string (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