X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGLocateInductive.ml;h=04181fb238a27be16f6887782251c58bc488dba6;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=04a2f2ad4806f016479dcceb1cafa81d7ceebb75;hpb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml
index 04a2f2ad4..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 = MQueryUtil.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
@@ -38,5 +38,3 @@ let get_constraints = function
       let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in
       (constr_obj, constr_rel, constr_sort)
    | _                      -> raise NotAnInductiveDefinition
-
-let universe = CGSearchPattern.universe