| Left -> current_size + 4
| LetIn (term, ident) ->
countterm (current_size + 5 + String.length ident) term
- | Reduce (_, _, _) -> assert false (* TODO *)
+ | Reduce (_, _) -> assert false (* TODO *)
| Reflexivity -> current_size + 11
| Replace (t1, t2) ->
let size1 = countterm (current_size + 14) t1 in (* replace, with *)
let string_of_kind = function
| `Reduce -> "reduce"
- | `Simpl -> "simpl"
+ | `Simpl -> "simplify"
| `Whd -> "whd"
let dummy_tbl = Hashtbl.create 0
Box.smallskip;
Box.Text([],"=")]);
Box.indent (ast2astBox term)])
- | Reduce (_, _, _) -> assert false (* TODO *)
+ | Reduce (_, _) -> assert false (* TODO *)
| Reflexivity -> Box.Text([],"reflexivity")
| Replace (t1, t2) ->
Box.V([],