new options activated

[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 ac873ec6677dd24cdc27c8745edb996b6baea16f..5153ced0765a57d98d7fab2dd27183e237d07936 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgOutput.ml
+++ b/helm/software/helena/src/basic_rg/brgOutput.ml
@@ -63,9 +63,9 @@ let rec count_term_binder f c e = function
       f c
 
 and count_term f c e = function
-   | B.Sort _         -> 
+   | B.Sort _            ->
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | B.LRef (_, i)    -> 
+   | B.LRef (_, i)       ->
       begin match B.get e i with
         | _, _, _, B.Abst _
         | _, _, _, B.Void   ->
@@ -73,22 +73,22 @@ and count_term f c e = function
         | _, _, _, B.Abbr _ ->
            f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
       end      
-   | B.GRef (_, u)    -> 
+   | B.GRef (_, u)       -> 
       let c =    
         if Cps.list_mem ~eq:U.eq u c.uris
         then {c with nodes = succ c.nodes}
         else {c with xnodes = succ c.xnodes}
       in
       f {c with tgrefs = succ c.tgrefs}
-   | B.Cast (_, v, t) -> 
+   | B.Cast (_, v, t)    -> 
       let c = {c with tcasts = succ c.tcasts} in
       let f c = count_term f c e t in
       count_term f c e v
-   | B.Appl (_, v, t) -> 
+   | B.Appl (_, _, v, t) -> 
       let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
       let f c = count_term f c e t in
       count_term f c e v
-   | B.Bind (a, b, t) -> 
+   | B.Bind (a, b, t)    -> 
       let f c = count_term f c (B.push e B.empty a b) t in
       count_term_binder f c e b
 
@@ -155,12 +155,12 @@ let rec pp_term st e och = function
       KP.fprintf och "$%s" (U.string_of_uri s)
    | B.Cast (_, u, t)                ->
       KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
-   | B.Appl (_, v, 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 (x, n, w), t) ->
+   | B.Bind (a, B.Abst (r, n, w), t) ->
       let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst x n w) in
-      KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced x (name C.start) a (pp_term st e) w (pp_term st ee) t
+      let ee = B.push e B.empty a (B.abst r n w) in
+      KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t
    | B.Bind (a, B.Abbr v, t)         ->
       let a = R.alpha B.mem e a in
       let ee = B.push e B.empty a (B.abbr v) in