(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+(* $Id$ *)
+
module T = MQGTypes
let text_of_entries out entries =
| 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) =