"(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 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
) connames_and_argsno_and_patterns)) ^
")\n")))
| C.Fix (no, funs) ->
- let names =
- List.rev
- (List.map
- (function (name,_,ty,_) ->
- Some (C.Name name,Cic.Decl ty)) funs)
+ let names,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) funs
in
"let rec " ^
List.fold_right
Some (Cic.Name n,_) -> n
| _ -> assert false)
| C.CoFix (no,funs) ->
- let names =
- List.rev
- (List.map
- (function (name,ty,_) ->
- Some (C.Name name,Cic.Decl ty)) funs)
+ let names,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) funs
in
"\nCoFix " ^ " {" ^
List.fold_right