let string_of_sort = function
| `Prop -> "Prop"
| `Set -> "Set"
- | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
+ | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
| `CProp -> "CProp"
let sort_of_sort = function
let xxx_type_of_aux' m c t =
let res,_ =
try
- CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph
with
| CicTypeChecker.AssertFailure _
| CicTypeChecker.TypeCheckerFailure _ ->
- Cic.Sort Cic.Prop, CicUniv.empty_ugraph
+ Cic.Sort Cic.Prop, CicUniv.oblivion_ugraph
in
res
;;