]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgOutput.ml
improved interface for brgEnvironment
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml
index dcefefa2efb758ca1922bceca594573bce6427f0..e29b3f4953bddeead3251d5c46957e7c5b361589 100644 (file)
@@ -58,13 +58,13 @@ let count_obj_binder f c = function
    | B.Abst -> f {c with eabsts = succ c.eabsts}
    | B.Abbr -> f {c with eabbrs = succ c.eabbrs}
 
-let count_obj f c (b, t) =
+let count_obj f c (_, _, b, t) =
    let f c = count_obj_binder f c b in
    count_term f c t
 
 let count_item f c = function
-   | Some (obj, _) -> count_obj f c obj
-   | None          -> f c
+   | Some obj -> count_obj f c obj
+   | None     -> f c
 
 let print_counters f c =
    let terms =