X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=a38ecde4c32051d8d2677b3010ce39ece9ca49af;hb=dac4721470c5db03f4291adfb4f73e2016040d4b;hp=e8177755c79a15faf12b7c9ee09f5d82881b98e2;hpb=85da1aebda823a6215271b9081cc20675616a126;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index e8177755c..a38ecde4c 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -14,23 +14,23 @@ module R = NReference
 let r2s pp_fix_name r = 
   try
     match r with
-    | R.Ref (_,u,R.Ind i) -> 
-        (match snd(NCicEnvironment.get_obj u) with
+    | R.Ref (_,u,R.Ind (_,i)) -> 
+        (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