Cic.Prop -> T.Prop
| Cic.Set -> T.Set
| Cic.Type -> T.Type
+ | Cic.CProp -> T.CProp
in
[],[],[!!kind,s']
| _ -> [],[],[])
| C.Meta _
- | C.Implicit -> assert false
+ | C.Implicit _ -> assert false
| C.Cast (te,_) ->
(* type ignored *)
process_type_aux kind te
) sorts ;
res
;;
+
+let universe =
+ [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]