- let c = {c with tappls = succ c.tappls} in
- let f c = count_term f c t in
- count_term f c v
- | B.Bind (_, b, t) ->
- let f c = count_term_binder f c b in
- count_term f c t
-
-let count_obj_binder f c = function
- | B.Abst w ->
- let c = {c with eabsts = succ c.eabsts} in
- count_term f c w
- | B.Abbr v ->
- let c = {c with eabbrs = succ c.eabbrs} in
- count_term f c v
- | B.Void -> f c
-
-let count_obj f c (_, _, b) =
- count_obj_binder f c b
+ let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
+ let f c = count_term f c e t in
+ count_term f c e v
+ | B.Bind (a, b, t) ->
+ let f c e = count_term f c e t in
+ let f c = B.push (f c) e a b in
+ count_term_binder f c e b
+
+let count_obj f c = function
+ | (_, u, B.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_context w
+ | (_, _, B.Abbr v) ->
+ let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
+ count_term f c B.empty_context v
+ | (_, _, B.Void) ->
+ let c = {c with evoids = succ c.evoids; xnodes = succ c.xnodes} in
+ f c