let rec aux =
function
Cic.Sort s -> `Sort s
- | Cic.Prod (_,_,t)
- | Cic.Lambda (_,_,t) -> aux t
+ | Cic.Prod (_,_,t) -> aux t
| _ -> `SomethingElse
in
match aux t with
let reserved =
[ "to";
"mod";
- "val"
+ "val";
+ "in";
+ "function"
]
in
function n ->
"(function " ^ ppname b ^ " -> " ^
pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
| C.LetIn (b,s,t) ->
- let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
+ let ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in
"(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
| C.Appl (C.MutInd _ as he::tl) ->
let rec aux argsno context =
function
Cic.Lambda (name,ty,bo) when argsno > 0 ->
+ let name =
+ match name with
+ Cic.Anonymous -> Cic.Anonymous
+ | Cic.Name n -> Cic.Name (ppid n) in
let args,res =
aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
bo