let t' = CicUniv.fresh() in
let ugraph1 = CicUniv.add_gt t' t ugraph in
(C.Sort (C.Type t')),ugraph1
- (* TASSI: CONSTRAINTS *)
| C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
- | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+ | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
| C.Cast (te,ty) as t ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in
let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in