From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 15 Oct 2004 14:08:45 +0000 (+0000)
Subject: moved string_of_uriref to UriManager
X-Git-Tag: V_0_0_10~72
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0694dd98ca6dbc0c5aa3a1d42a6316b083b3be7c;p=helm.git

moved string_of_uriref to UriManager
---

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml
index c5734f242..04181fb23 100644
--- a/helm/ocaml/mathql_generator/cGLocateInductive.ml
+++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml
@@ -30,7 +30,7 @@ exception NotAnInductiveDefinition
 
 let get_constraints = function
    | Cic.MutInd (uri, t, _) -> 
-      let uri = MQueryMisc.string_of_uriref (uri, [t]) in
+      let uri = UriManager.string_of_uriref (uri, [t]) in
       let constr_obj =
        [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
       in
diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 8d6aed908..7304b39f5 100644
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -64,7 +64,7 @@ let levels_of_term metasenv context term =
    in
    let inspect_uri main l uri tc v term =
       let d = degree term in 
-      entry_in (Misc.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
+      entry_in (UriManager.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
    in
    let rec inspect_term main l v term = match term with
         Cic.Rel _                        -> l