]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgOutput.ml
- new attributes system
[helm.git] / helm / software / helena / src / basic_rg / brgOutput.ml
index 978658caa0cd6fbf87d144a1275b3e1e877dccbe..aa3cce9524c9719d516dd27e6dad5e0d60db00ab 100644 (file)
@@ -91,15 +91,15 @@ and count_term f c e = function
       count_term_binder f c e b
 
 let count_entity f c = function
-   | _, u, E.Abst (_, w) -> 
+   | _, _, u, E.Abst w -> 
       let c = {c with
          eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
       } in
       count_term f c B.empty w
-   | _, _, E.Abbr v      ->  
+   | _, _, _, E.Abbr v ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c B.empty v
-   | _, _, E.Void        -> assert false
+   | _, _, _, E.Void   -> assert false
 
 let print_counters f c =
    let terms =
@@ -143,7 +143,7 @@ let rename f e a =
       does_not_occur f n r e
    in
    let f n0 r0 =
-      let f n r = if n = n0 && r = r0 then f a else f (E.Name (n, r) :: a) in
+      let f n r = if n = n0 && r = r0 then f a else f {a with E.n_name = Some (n, r)} in
       aux f e n0 r0 
    in
    E.name C.err f a
@@ -158,7 +158,7 @@ let name err och a =
    E.name err f a
 
 let pp_level och n =
-   if N.is_infinite n then () else P.fprintf och "^%s" (N.to_string n)
+   P.fprintf och "%s" (N.to_string n)
 
 let rec pp_term e och = function
    | B.Sort (_, h)           ->