- 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) ^ ")"
+ (match analyze_term context s with
+ `Type
+ | `Proof ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph
+ in
+ pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context)
+ | `Term ->
+ 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 (he::tl) when in_type ->
+ let hes = pp ~in_type he context in
+ let stl = String.concat "," (clean_args_for_ty context tl) in
+ (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes