- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / complete_rg / crgOutput.ml

diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
index efa39eec6d7fe6878140def53346933696d3da01..0b3964258cb9721ed141a3ded0c271920ef28869 100644 (file)
--- 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           -> ()