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
| 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) =