From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 12:38:49 +0000 (+0000)
Subject: removed reference to MQueryMisc
X-Git-Tag: V_0_0_10~33
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ff32595bcb09272afe9be4143062da85354c14dd;p=helm.git

removed reference to MQueryMisc
---

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 7304b39f5..1e721a456 100644
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -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