- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 529a293e1a79d737d8775a9ec96f51e83330dcc9..3ad78a37be6f22835e65140deb3347ed9042478b 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -134,23 +134,23 @@ let pp_attrs out a =
    let f i = out (P.sprintf "+%i;" i) in
    E.apix ignore f a
 
-let rec pp_term out = function
+let rec pp_term out st = function
    | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
    | D.TLRef (a, i   ) -> pp_attrs out a; out (P.sprintf "#%u" i)
    | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
-   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
-   | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out x; out ")."; pp_term out y
-   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; out "."; pp_term out y
-   | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out x; out "}."; pp_term out y
+   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
+   | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
+   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
+   | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out st x; out "}."; pp_term out st y
 
-and pp_bind out = function
+and pp_bind out st = function
    | D.Abst (n, x) ->
-      out "[:"; pp_term out x; out "]"; out (N.to_string n)  
-   | D.Abbr x      -> out "[="; pp_term out x; out "]";
+      out "[:"; pp_term out st x; out "]"; out (N.to_string st n)  
+   | D.Abbr x      -> out "[="; pp_term out st x; out "]";
    | D.Void        -> out "[]"
 
-and pp_lenv out = function
+and pp_lenv out st = function
    | D.ESort           -> ()
-   | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
-   | D.EAppl (x, a, y) -> pp_lenv out x; out "("; pp_term out y; out ")"
-   | D.EProj (x, a, y) -> pp_lenv out x; out "{"; pp_lenv out y; out "}"
+   | D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
+   | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ")"
+   | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "}"