X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagOutput.ml;h=41914b062caf82673450dc20705f16ce70356cca;hb=fec20705af4705f8eb9542aece87769b82a6a6b4;hp=88e64e5d05e343c3791898f920fd443f27816c8f;hpb=9935a5bf5bdc98ad01a2b0234cf4e612a62c939f;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml
index 88e64e5d0..41914b062 100644
--- a/helm/software/helena/src/basic_ag/bagOutput.ml
+++ b/helm/software/helena/src/basic_ag/bagOutput.ml
@@ -111,41 +111,41 @@ let res a l och =
    if !G.indexes then err () else name err och a
 
 let rec pp_term st c och = function
-   | Z.Sort h                 -> 
+   | Z.Sort h                   -> 
       let err () = KP.fprintf och "*%u" h in
       let f s = KP.fprintf och "%s" s in
       H.string_of_sort err f h 
-   | Z.LRef i                 -> 
+   | Z.LRef i                   -> 
       let err () = KP.fprintf och "#%s" (P.string_of_mark i) in
       let f a _ = name err och a in
       if !G.indexes then err () else Z.get err f c i
-   | Z.GRef s                    -> KP.fprintf och "$%s" (U.string_of_uri s)
-   | Z.Cast (u, t)               ->
+   | Z.GRef s                   -> KP.fprintf och "$%s" (U.string_of_uri s)
+   | Z.Cast (u, t)              ->
       KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
-   | Z.Appl (v, t)               ->
+   | Z.Appl (v, t)              ->
       KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
-   | Z.Bind (a, l, Z.Abst w, t) ->
+   | Z.Bind (y, l, Z.Abst w, t) ->
       let f cc =
-         KP.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t
+         KP.fprintf och "[%t:%a].%a" (res y l) (pp_term st c) w (pp_term st cc) t
       in
-      Z.push "output abst" f c a l (Z.Abst w)
-   | Z.Bind (a, l, Z.Abbr v, t) ->
+      Z.push "output abst" f c y l (Z.Abst w)
+   | Z.Bind (y, l, Z.Abbr v, t) ->
       let f cc = 
-         KP.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t
+         KP.fprintf och "[%t=%a].%a" (res y l) (pp_term st c) v (pp_term st cc) t
       in
-      Z.push "output abbr" f c a l (Z.Abbr v)
-   | Z.Bind (a, l, Z.Void, t)   ->
-      let f cc = KP.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in
-      Z.push "output void" f c a l Z.Void
+      Z.push "output abbr" f c y l (Z.Abbr v)
+   | Z.Bind (y, l, Z.Void, t)   ->
+      let f cc = KP.fprintf och "[%t].%a" (res y l) (pp_term st cc) t in
+      Z.push "output void" f c y l Z.Void
 
 let pp_lenv st och c =
    let pp_entry och = function
-      | a, l, Z.Abst w -> 
-         KP.fprintf och "%t : %a\n" (res a l) (pp_term st c) w
-      | a, l, Z.Abbr v -> 
-         KP.fprintf och "%t = %a\n" (res a l) (pp_term st c) v
-      | a, l, Z.Void   -> 
-         KP.fprintf och "%t\n" (res a l)
+      | y, l, Z.Abst w -> 
+         KP.fprintf och "%t : %a\n" (res y l) (pp_term st c) w
+      | y, l, Z.Abbr v -> 
+         KP.fprintf och "%t = %a\n" (res y l) (pp_term st c) v
+      | y, l, Z.Void   -> 
+         KP.fprintf och "%t\n" (res y l)
    in
    let iter map och l = List.iter (map och) l in
    let f es = KP.fprintf och "%a" (iter pp_entry) (List.rev es) in