new syntax of abstractions propagated to complete_rg

[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 b5b60e8fd5d8fd7c6a3167b918f6a7460274d31f..ac873ec6677dd24cdc27c8745edb996b6baea16f 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgOutput.ml
+++ b/helm/software/helena/src/basic_rg/brgOutput.ml
@@ -171,19 +171,18 @@ let rec pp_term st e och = function
       KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t
 
 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 a = R.alpha B.mem e a in
-         KP.fprintf och "%a : %a\n" (name C.start) a (pp_term st e) w; f a
-      | B.Abbr (a, v) ->
-         let a = R.alpha B.mem e a in
-         KP.fprintf och "%a = %a\n" (name C.start) a (pp_term st e) v; f a
-      | B.Void a      ->
-         let a = R.alpha B.mem e a in
-         KP.fprintf och "%a\n" (name C.start) a; f a
-*)   in
-   let e = B.empty in
-   if e = B.empty then KP.fprintf och "%s\n" "not shown" else
+   let pp_entry f c a b x =
+      let a = R.alpha B.mem e a in
+      let x = B.push x c a b in
+      match b with
+         | B.Abst (_, _, w) ->
+            KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x
+         | B.Abbr v            ->
+            KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x
+         | B.Void           ->
+            KP.fprintf och "[%a]" (name C.start) a; f x
+   in
+   if e = B.empty then KP.fprintf och "%s" "empty" else
    B.fold_right ignore pp_entry e B.empty
 
 let specs = {