- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / basic_rg / brgOutput.ml

diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml
index aa3cce9524c9719d516dd27e6dad5e0d60db00ab..fe67e2c7ba531912bdc8f6a412f67bdbea49c6ba 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgOutput.ml
+++ b/helm/software/helena/src/basic_rg/brgOutput.ml
@@ -157,10 +157,10 @@ let name err och a =
    in      
    E.name err f a
 
-let pp_level och n =
-   P.fprintf och "%s" (N.to_string n)
+let pp_level st och n =
+   P.fprintf och "%s" (N.to_string st n)
 
-let rec pp_term e och = function
+let rec pp_term st e och = function
    | B.Sort (_, h)           -> 
       let err _ = P.fprintf och "*%u" h in
       let f s = P.fprintf och "%s" s in
@@ -173,35 +173,35 @@ let rec pp_term e och = function
    | B.GRef (_, s)           ->
       P.fprintf och "$%s" (U.string_of_uri s)
    | B.Cast (_, u, t)        ->
-      P.fprintf och "{%a}.%a" (pp_term e) u (pp_term e) t
+      P.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
    | B.Appl (_, v, t)        ->
-      P.fprintf och "(%a).%a" (pp_term e) v (pp_term e) t
+      P.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
    | B.Bind (a, B.Abst (n, w), t) ->
       let f a =
          let ee = B.push e B.empty a (B.abst n w) in
-        P.fprintf och "[%a:%a]%a.%a" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t
+        P.fprintf och "%a[%a:%a].%a" (pp_level st) n (name C.err) a (pp_term st e) w (pp_term st ee) t
       in
       rename f e a
    | B.Bind (a, B.Abbr v, t) ->
       let f a = 
          let ee = B.push e B.empty a (B.abbr v) in
-        P.fprintf och "[%a=%a].%a" (name C.err) a (pp_term e) v (pp_term ee) t
+        P.fprintf och "[%a=%a].%a" (name C.err) a (pp_term st e) v (pp_term st ee) t
       in
       rename f e a
    | B.Bind (a, B.Void, t)   ->
       let f a = 
          let ee = B.push e B.empty a B.Void in
-         P.fprintf och "[%a].%a" (name C.err) a (pp_term ee) t
+         P.fprintf och "[%a].%a" (name C.err) a (pp_term st ee) t
       in
       rename f e a
 
-let pp_lenv och e =
+let pp_lenv st och e =
    let pp_entry f e c a b x = f x (* match b with
       | B.Abst (a, w) -> 
-         let f a = P.fprintf och "%a : %a\n" (name C.err) a (pp_term e) w; f a in
+         let f a = P.fprintf och "%a : %a\n" (name C.err) a (pp_term st e) w; f a in
          rename f x a
       | B.Abbr (a, v) -> 
-         let f a = P.fprintf och "%a = %a\n" (name C.err) a (pp_term e) v; f a in
+         let f a = P.fprintf och "%a = %a\n" (name C.err) a (pp_term st e) v; f a in
         rename f c a
       | B.Void a      -> 
          let f a = P.fprintf och "%a\n" (name C.err) a; f a in
@@ -217,5 +217,5 @@ let specs = {
 
 (* term xml printing ********************************************************)
 
-let export_term =
-   BD.crg_of_brg XD.export_term  
+let export_term st =
+   BD.crg_of_brg (XD.export_term st)