X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.ml;h=70dfde4755b1aa8ffed2ef4175943d6e2426d8d0;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1e721a456bf1d99795ea367d96032e04807ba431;hpb=ff32595bcb09272afe9be4143062da85354c14dd;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 1e721a456..70dfde475 100644
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -50,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) =