From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 15:12:30 +0000 (+0000)
Subject: better pp of objects
X-Git-Tag: make_still_working~5357
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=385fe4ef8b24dc17d2c6a214c9b025c5275f1d7e;p=helm.git

better pp of objects
---

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"