From 385fe4ef8b24dc17d2c6a214c9b025c5275f1d7e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 15:12:30 +0000 Subject: [PATCH] better pp of objects --- helm/software/components/ng_kernel/nCicPp.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 8bcbf6ad9..72e8abff5 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -139,8 +139,8 @@ let ppobj = function 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"^ @@ -149,9 +149,11 @@ let ppobj = function " | "^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" -- 2.39.2