]>
matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/cGSearchPattern.ml
| 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']
| _ -> [],[],[])