X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;h=0b3964258cb9721ed141a3ded0c271920ef28869;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=efa39eec6d7fe6878140def53346933696d3da01;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
index efa39eec6..0b3964258 100644
--- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
@@ -14,6 +14,7 @@ module U = NUri
 module C = Cps
 module H = Hierarchy
 module E = Entity
+module N = Level
 module D = Crg
 
 (****************************************************************************)
@@ -47,9 +48,11 @@ and pp_terms bg eg out vs =
    out bg; aux vs; out (eg ^ ".")
 
 and pp_bind out = function
-   | D.Abst x -> pp_terms "[:" "]" out x
-   | D.Abbr x -> pp_terms "[=" "]" out x
-   | D.Void x -> out (P.sprintf "[%u]" x)
+   | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x
+   | D.Abst (n, x)                      -> 
+      pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x
+   | D.Abbr x                           -> pp_terms "[=" "]" out x
+   | D.Void x                           -> out (P.sprintf "[%u]" x)
 
 let rec pp_lenv out = function
    | D.ESort           -> ()