LocatedTactic (_, tac) -> count_tactic current_size tac
| Absurd term -> countterm (current_size + 6) term
| Apply term -> countterm (current_size + 6) term
LocatedTactic (_, tac) -> count_tactic current_size tac
| Absurd term -> countterm (current_size + 6) term
| Apply term -> countterm (current_size + 6) term
| Assumption -> current_size + 10
| Change (t1, t2, where) ->
let size1 = countterm (current_size + 12) t1 in (* change, with *)
| Assumption -> current_size + 10
| Change (t1, t2, where) ->
let size1 = countterm (current_size + 12) t1 in (* change, with *)
| Injection ident -> current_size + 10 + (String.length ident)
| Intros (num, idents) ->
List.fold_left
| Injection ident -> current_size + 10 + (String.length ident)
| Intros (num, idents) ->
List.fold_left
| Reflexivity -> current_size + 11
| Replace (t1, t2) ->
let size1 = countterm (current_size + 14) t1 in (* replace, with *)
| Reflexivity -> current_size + 11
| Replace (t1, t2) ->
let size1 = countterm (current_size + 14) t1 in (* replace, with *)
Box.V([],[Box.Text([],"apply");
ast2astBox term])
| Assumption -> Box.Text([],"assumption")
Box.V([],[Box.Text([],"apply");
ast2astBox term])
| Assumption -> Box.Text([],"assumption")
Box.Text([],string_of_kind kind)]);
Box.indent(ast2astBox term)])
| Fourier -> Box.Text([],"fourier")
Box.Text([],string_of_kind kind)]);
Box.indent(ast2astBox term)])
| Fourier -> Box.Text([],"fourier")
| Injection ident ->
Box.V([],[Box.Text([],"transitivity");
Box.indent (Box.Text([],ident))])
| Injection ident ->
Box.V([],[Box.Text([],"transitivity");
Box.indent (Box.Text([],ident))])