| Branch _ ->
let s' =
match s with
- Cic.Prop -> T.Prop
- | Cic.Set -> T.Set
- | Cic.Type -> T.Type
+ Cic.Prop -> T.Prop
+ | Cic.Set -> T.Set
+ | Cic.CProp -> T.CProp
+ | Cic.Type -> T.Type
in
[],[],[!!kind,s']
| _ -> [],[],[])
) sorts ;
res
;;
+
+let universe =
+ [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]