]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/complete_rg/crgOutput.ml
update in helena
[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml
index 535ec2bebccd5e8dc8f8ffd81d6c1f4e118c16c0..f068181a789e034488563d970cde256d181d0969 100644 (file)
@@ -94,15 +94,15 @@ and count_binder f c e y b = match b with
       D.push_bind (f c) E.empty_node y b e
 
 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 D.ESort w
-   | _, _, _, E.Abbr v ->  
+   | _, _, _, E.Abbr (_, v) ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c D.ESort v
-   | _, _, _, E.Void   -> assert false
+   | _, _, _, E.Void        -> assert false
 
 let print_counters f c =
    let terms =