moved string_of_uriref to UriManager

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml
index c5734f2429a173a61c2c7ffd0530339a5a9f1560..04181fb238a27be16f6887782251c58bc488dba6 100644 (file)
--- 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 8d6aed90818268acaae7238b4bf6433576195c4c..7304b39f5c12d99221d27e021e1043155e54f6ef 100644 (file)
--- 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