X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.ml;h=70dfde4755b1aa8ffed2ef4175943d6e2426d8d0;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7304b39f5c12d99221d27e021e1043155e54f6ef;hpb=0694dd98ca6dbc0c5aa3a1d42a6316b083b3be7c;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 7304b39f5..70dfde475 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 
@@ -51,7 +50,7 @@ let levels_of_term metasenv context term =
          | Cic.Prod (_, _, t) -> degree_aux t
          | _                  -> 2
       in 
-      let u = TC.type_of_aux' metasenv context t in
+      let u,_ = TC.type_of_aux' metasenv context t CicUniv.empty_ugraph in
       degree_aux (Red.whd context u)
    in
    let entry_eq (s1, b1, v1) (s2, b2, v2) =