C.Anonymous ->
(*CSC: great space for improvements here *)
(try
- (match CicTypeChecker.type_of_aux' ~subst metasenv context typ with
+ let ty,_ =
+ CicTypeChecker.type_of_aux' ~subst metasenv context typ
+ CicUniv.empty_ugraph in
+ (match ty with
C.Sort C.Prop
| C.Sort C.CProp -> "H"
| C.Sort C.Set -> "x"