]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/toplevel/metaOutput.ml
- initial support for abstractions with explicit levels
[helm.git] / helm / software / lambda-delta / src / toplevel / metaOutput.ml
index 2d9246f5dd407bb0c195c3506b82ceff9bad7a2a..0f25e13e5f19555e0fd176900601657cd751f65c 100644 (file)
@@ -69,21 +69,21 @@ let count_xterm f c = function
    | Some v -> count_term f c v
 
 let count_entity f c = function
-   | _, u, E.Abst (pars, w, xv) ->
+   | _, u, E.Abst (_, (pars, w, xv)) ->
       let c = {c with eabsts = succ c.eabsts} in
       let c = {c with pabsts = c.pabsts + List.length pars} in
       let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in
       let f c = count_xterm f c xv in      
       let f c = count_term f c w in
       Cps.list_fold_left f count_par c pars   
-   | _, _, E.Abbr (pars, w, xv) ->
+   | _, _, E.Abbr (pars, w, xv)      ->
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       let c = {c with pabsts = c.pabsts + List.length pars} in
       let c = {c with nodes = c.nodes + List.length pars} in
       let f c = count_xterm f c xv in
       let f c = count_term f c w in
       Cps.list_fold_left f count_par c pars
-   | _, _, E.Void               -> assert false
+   | _, _, E.Void                    -> assert false
 
 let print_counters f c =
    let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in