X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=6a642390efb1a949d91170bc8e368ce1ae52befd;hb=2c26d3c2140cfc213c960568587f8350e34d3459;hp=4f3892cbc992f9e6738136f05163254ab3283404;hpb=ceac1e90a8108f526e33bbae7173571c55ea802d;p=helm.git

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 4f3892cbc..6a642390e 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -796,15 +796,15 @@ type term_former_decl = term_context * typ
 
 let rec pp_obj status (uri,obj_kind) =
   let pretty_print_context ctx =
-    String.concat " " (List.rev
+    String.concat " " (List.rev (snd
       (List.fold_right
-       (fun (x,kind) l ->
+       (fun (x,kind) (l,res) ->
          let x,l = x @:::l in
          if size_of_kind kind > 1 then
-          ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l
+          x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
          else
-          x::l)
-       (HExtlib.filter_map (fun x -> x) ctx) []))
+          x::l,x::res)
+       (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
   in
  let namectx_of_ctx ctx =
   List.fold_right (@::)