]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/cGMatchConclusion.ml
renamed Http_client to Http_user_agent to avoid clashes with Gerd's
[helm.git] / helm / ocaml / mathql_generator / cGMatchConclusion.ml
index 8d6aed90818268acaae7238b4bf6433576195c4c..1e721a456bf1d99795ea367d96032e04807ba431 100644 (file)
@@ -43,7 +43,6 @@ let sort_entries entries =
 let levels_of_term metasenv context term =
    let module TC = CicTypeChecker in
    let module Red = CicReduction in
-   let module Misc = MQueryMisc in
    let degree t =
       let rec degree_aux = function
          | Cic.Sort _         -> 1 
@@ -64,7 +63,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