X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=878740c0c375bcc7a2637d1361b446d6be9618cd;hb=32522cf70b6bc38f0c3cc5d25b9bd1a93f05862f;hp=782fd9566ba53f5af38a7825b31eec1d7bd10262;hpb=13553fb82419f58ab61131bd4a6e04352e388b50;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 782fd9566..878740c0c 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -15,22 +15,22 @@ let r2s pp_fix_name r =
   try
     match r with
     | R.Ref (_,u,R.Ind i) -> 
-        (match snd(NCicEnvironment.get_obj u) with
+        (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,name,_,_ = List.nth itl i in name
         | _ -> assert false)
     | R.Ref (_,u,R.Con (i,j)) -> 
-        (match snd(NCicEnvironment.get_obj u) with
+        (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,_,_,cl = List.nth itl i in
             let _,name,_ = List.nth cl (j-1) in name
         | _ -> assert false)
     | R.Ref (_,u,(R.Decl | R.Def )) -> 
-        (match snd(NCicEnvironment.get_obj u) with
+        (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Constant (_,name,_,_,_) -> name
         | _ -> assert false)
     | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
-        (match snd(NCicEnvironment.get_obj u) with
+        (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Fixpoint (_,fl,_) -> 
             if pp_fix_name then
               let _,name,_,_,_ = List.nth fl i in name
@@ -134,7 +134,7 @@ let trivial_pp_term ~context ~subst ~metasenv ?(inside_fix=false) t =
 let ppobj = function
   | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) -> 
       "{"^NUri.string_of_uri u^"}\n"^
-      "let rec "^
+      (if b then "let rec " else "let corec ") ^
        String.concat "\nand " 
         (List.map (fun (_,name,n,ty,bo) ->
           name^ " on " ^ string_of_int n ^ " : " ^ 
@@ -160,3 +160,14 @@ let ppobj = function
           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"
+;;