UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
| C.Meta (n,l1) ->
"?" ^ (string_of_int n) ^ "[" ^
-(*
String.concat " ; "
(List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-*)
"]"
| C.Sort s ->
(match s with
| 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.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+ | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
)
| C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
| C.LetIn (b,s,t) ->
- "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+ " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right