| C.Prod ("_",s,t) ->
if not toplevel then F.fprintf f "(";
F.fprintf f "@[<hov 1>";
- aux ~toplevel:true ctx s;
+ (match s with
+ | C.Prod ("_",_,_) -> aux ~toplevel:false ctx s
+ | _ -> aux ~toplevel:true ctx s);
F.fprintf f "@;→ ";
aux ~toplevel:true ("_"::ctx) t;
F.fprintf f "@]";
ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
| (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- "inductive ("^string_of_int leftno^") "^
+ "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
+ "inductive "^
String.concat "\nand "
(List.map (fun (_,name,ty,cl) ->
name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
" | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
cl)) tyl) ^ "."
| (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) ->
+ "{"^NUri.string_of_uri u^"}\n"^
"axiom " ^ name ^ " : " ^
ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
| (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
+ "{"^NUri.string_of_uri u^"}\n"^
"definition " ^ name ^ " : " ^
ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
;;
+
+let rec ppcontext ~subst ~metasenv = function
+ | [] -> ""
+ | (name, NCic.Decl t) :: tl ->
+ ppcontext ~subst ~metasenv tl ^
+ name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl t ^ "\n"
+ | (name, NCic.Def (bo,ty)) :: tl->
+ ppcontext ~subst ~metasenv tl ^
+ name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl ty ^
+ " := " ^ ppterm ~subst ~metasenv ~context:tl bo ^ "\n"
+;;