| Left _ -> current_size + 4
| LetIn (_, term, ident) ->
countterm (current_size + 5 + String.length ident) term
- | Reduce _ -> assert false (* TODO *)
+ | Reduce _
+ | ReduceAt _ -> assert false (* TODO *)
| Reflexivity _ -> current_size + 11
| Replace (_, t1, t2) ->
let size1 = countterm (current_size + 14) t1 in (* replace, with *)
Box.smallskip;
Box.Text([],"=")]);
Box.indent (ast2astBox term)])
- | Reduce _ -> assert false (* TODO *)
+ | Reduce _
+ | ReduceAt _ -> assert false (* TODO *)
| Reflexivity _ -> Box.Text([],"reflexivity")
| Replace (_, t1, t2) ->
Box.V([],