new options activated

[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 dc5d78ce1f8f8dcb9f47d0aac9390fd7c2f7bf2d..95c3e8801a41ead8dd99d758b8603ec4b803b05c 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -48,33 +48,33 @@ let initial_counters = {
 }
 
 let rec count_term f c e = function
-   | D.TSort _          -> 
+   | D.TSort _            -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | D.TLRef (_, i)     -> 
+   | D.TLRef (_, i)       -> 
       begin match D.get e i with
         | _, _, D.Abbr _ ->
            f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
         | _              ->
            f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
       end      
-   | D.TGRef (_, u)     -> 
+   | D.TGRef (_, u)       -> 
       let c =    
         if C.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}
-   | D.TCast (_, v, t)  -> 
+   | D.TCast (_, 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
-   | D.TAppl (_, v, t)  -> 
+   | D.TAppl (_, _, v, t) -> 
       let c = {c with tappls = succ c.tappls} in
       let f c = count_term f c e t in
       count_term f c e v
-   | D.TProj (_, d, t)  ->
+   | D.TProj (_, d, t)    ->
       D.shift (count_term f c e) d t
-   | D.TBind (a, b, t)  -> 
+   | D.TBind (a, b, t)    -> 
       let f c e = count_term f c e t in
       count_binder f c e a b
 
@@ -137,22 +137,22 @@ let pp_attrs out a =
 let pp_state out x = if x then out "^"
 
 let rec pp_term out st = function
-   | D.TSort (a, l)    -> pp_attrs out a; out (KP.sprintf "*%u" l)
-   | D.TLRef (a, i   ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
-   | D.TGRef (a, u)    -> pp_attrs out a; out (KP.sprintf "$")
-   | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
-   | D.TAppl (a, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
-   | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
-   | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
+   | D.TSort (a, l)       -> pp_attrs out a; out (KP.sprintf "*%u" l)
+   | D.TLRef (a, i   )    -> pp_attrs out a; out (KP.sprintf "#%u" i)
+   | D.TGRef (a, u)       -> pp_attrs out a; out (KP.sprintf "$")
+   | D.TCast (a, u, t)    -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
+   | D.TAppl (a, _, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
+   | D.TBind (a, u, t)    -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
+   | D.TProj (a, u, t)    -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
 
 and pp_bind out st = function
-   | D.Abst (x, n, u) ->
-      out "[:"; pp_term out st u; out "]"; pp_state out x; out (N.to_string st n); out " "  
+   | D.Abst (r, n, u) ->
+      out "[:"; pp_term out st u; out "]"; pp_state out r; out (N.to_string st n); out " "  
    | D.Abbr u         -> out "[="; pp_term out st u; out "] ";
    | D.Void           -> out "[] "
 
 and pp_lenv out st = function
-   | D.ESort           -> ()
-   | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
-   | D.EAppl (u, a, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
-   | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
+   | D.ESort              -> ()
+   | D.EBind (u, a, t)    -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
+   | D.EAppl (u, a, _, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+   | D.EProj (u, a, t)    -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "