-
-let ppobj = function
- | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- (if b then "let rec " else "let corec ") ^
- String.concat "\nand "
- (List.map (fun (_,name,n,ty,bo) ->
- name^ " on " ^ string_of_int n ^ " : " ^
- 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^"} with "^string_of_int leftno^" fixed params\n"^
- (if b then "inductive " else "coinductive ")^
- String.concat "\nand "
- (List.map (fun (_,name,ty,cl) ->
- name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
- String.concat "\n"
- (List.map (fun (_,name,ty) ->
- " | "^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"
-;;
-