]> matita.cs.unibo.it Git - helm.git/commitdiff
removed reference to MQueryMisc
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 22 Oct 2004 12:38:49 +0000 (12:38 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 22 Oct 2004 12:38:49 +0000 (12:38 +0000)
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