]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_ag/bagOutput.ml
new options activated
[helm.git] / helm / software / helena / src / basic_ag / bagOutput.ml
index 88e64e5d05e343c3791898f920fd443f27816c8f..4867c7180d53198af018af0853c0157be9f2d06f 100644 (file)
@@ -111,18 +111,18 @@ 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) ->
       let f cc =