]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgOutput.ml
command line options rearranged
[helm.git] / helm / software / helena / src / basic_rg / brgOutput.ml
index 5153ced0765a57d98d7fab2dd27183e237d07936..6a40aecd4df2c87a09a596cf5378e0352bdb7229 100644 (file)
@@ -9,6 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module KF = Filename
 module KP = Printf
 
 module U  = NUri
@@ -152,9 +153,10 @@ let rec pp_term st e och = function
       let _, _, a, b = B.get e i in
       KP.fprintf och "%a" (name err) a
    | B.GRef (_, s)                   ->
-      KP.fprintf och "$%s" (U.string_of_uri s)
+      let u = U.string_of_uri s in
+      KP.fprintf och "$%s" (if !G.short then KF.basename u else u)
    | B.Cast (_, u, t)                ->
-      KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
+      KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t
    | B.Appl (_, _, v, t)             ->
       KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
    | B.Bind (a, B.Abst (r, n, w), t) ->