(match s with
C.Prop -> "Prop"
| C.Set -> "Set"
- | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
+ | C.Type _ -> "Type"
+ (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
| C.CProp -> "CProp"
)
+ | C.Implicit (Some `Hole) -> "%"
| C.Implicit _ -> "?"
| C.Prod (b,s,t) ->
(match b with
C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
| C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
)
- | C.Cast (v,t) -> pp v l
+ | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
| C.LetIn (b,s,t) ->