X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGLocateInductive.ml;h=261b293884f28a1399a890f86d7c138f56cc30bf;hb=be5869cd0bbe16c8a67827723c97d2d4fce4c0bc;hp=c5734f2429a173a61c2c7ffd0530339a5a9f1560;hpb=68e62a195d6228befb75b4e2edd59bc58b1cdb0c;p=helm.git diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml index c5734f242..261b29388 100644 --- a/helm/ocaml/mathql_generator/cGLocateInductive.ml +++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml @@ -26,11 +26,13 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + 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