X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGLocateInductive.ml;h=04181fb238a27be16f6887782251c58bc488dba6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=032060fd3d7d4736f1696188c7cd367a2527911e;hpb=36d9dada5eb3894d96c807781e1056b73a1c0a79;p=helm.git diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml index 032060fd3..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