- LocatedTactic (_, tac) -> count_tactic current_size tac
- | Absurd term -> countterm (current_size + 6) term
- | Apply term -> countterm (current_size + 6) term
- | Auto -> current_size + 4
- | Assumption -> current_size + 10
- | Change (t1, t2, where) ->
- let size1 = countterm (current_size + 12) t1 in (* change, with *)
- let size2 = countterm size1 t2 in
- (match where with
- None -> size2
- | Some ident -> size2 + 3 + String.length ident)
- | Change_pattern (_, _, _) -> assert false (* TODO *)
- | Contradiction -> current_size + 13
- | Cut term -> countterm (current_size + 4) term
- | Decompose (ident, principles) ->
- List.fold_left
- (fun size s -> size + (String.length s))
- (current_size + 11 + String.length ident) principles
- | Discriminate ident -> current_size + 12 + (String.length ident)
- | Elim (term, using) ->
+ | Absurd (_, term) -> countterm (current_size + 6) term
+ | Apply (_, term) -> countterm (current_size + 6) term
+ | Auto _ -> current_size + 4
+ | Assumption _ -> current_size + 10
+ | Compare (_, term) -> countterm (current_size + 7) term
+ | Constructor (_, n) -> current_size + 12
+ | Contradiction _ -> current_size + 13
+ | Cut (_, ident, term) ->
+ let id_size =
+ match ident with
+ None -> 0
+ | Some id -> String.length id + 4
+ in
+ countterm (current_size + 4 + id_size) term
+ | DecideEquality _ -> current_size + 15
+ | Decompose (_, term) ->
+ countterm (current_size + 11) term
+ | Discriminate (_, term) -> countterm (current_size + 12) term
+ | Elim (_, term, using) ->