match s with
Cic.Prop -> T.Prop
| Cic.Set -> T.Set
- | Cic.Type -> T.Type
+ | Cic.Type _ -> T.Type (* TASSI: ?? *)
| Cic.CProp -> T.CProp
in
[],[],[!!kind,s']
| _ -> [],[],[])
- | C.Meta _
- | C.Implicit -> assert false
+ | C.Meta _ -> [],[],[] (* ???? To be understood *)
+ | C.Implicit _ -> assert false
| C.Cast (te,_) ->
(* type ignored *)
process_type_aux kind te