more strings to UriManager.uri

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a74df9313cc5a05755e1a883f836dfe0cb4d92e6..14eab882c80dc39f942def9de4d0a052e962c38f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -212,11 +212,11 @@ let eval_coercion status coercion =
   let context = [] in 
   let src_uri = 
     let ty_src = CicReduction.whd context ty_src in
-    UriManager.uri_of_string (CicUtil.uri_of_term ty_src) 
+     CicUtil.uri_of_term ty_src
   in
   let tgt_uri = 
     let ty_tgt = CicReduction.whd context ty_tgt in
-    UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) 
+     CicUtil.uri_of_term ty_tgt
   in
   let new_coercions =
     (* also adds them to the Db *)
@@ -288,7 +288,7 @@ let eval_command status cmd =
           {status with aliases = 
             DisambiguateTypes.Environment.add 
               (DisambiguateTypes.Id id) 
-              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) 
+              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
               status.aliases }
       | TacticAst.Symbol_alias (symb, instance, desc) ->
           {status with aliases =