]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/cGMatchConclusion.ml
removed reference to MQueryMisc
[helm.git] / helm / ocaml / mathql_generator / cGMatchConclusion.ml
index 7304b39f5c12d99221d27e021e1043155e54f6ef..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