From 0694dd98ca6dbc0c5aa3a1d42a6316b083b3be7c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 15 Oct 2004 14:08:45 +0000 Subject: [PATCH] moved string_of_uriref to UriManager --- helm/ocaml/mathql_generator/cGLocateInductive.ml | 2 +- helm/ocaml/mathql_generator/cGMatchConclusion.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2