(match where with
None -> size2
| Some ident -> size2 + 3 + String.length ident)
- | Change_pattern _ -> assert false (* TODO *)
+(* | Change_pattern _ -> assert false (* TODO *) *)
| Contradiction _ -> current_size + 13
| Cut (_, term) -> countterm (current_size + 4) term
| Decompose (_, ident, principles) ->
| Left _ -> current_size + 4
| LetIn (_, term, ident) ->
countterm (current_size + 5 + String.length ident) term
- | Reduce _
- | ReduceAt _ -> assert false (* TODO *)
+(* | Reduce _ *)
+ | Reduce _ -> assert false (* TODO *)
| Reflexivity _ -> current_size + 11
| Replace (_, t1, t2) ->
let size1 = countterm (current_size + 14) t1 in (* replace, with *)
countterm size1 t2
- | Replace_pattern _ -> assert false (* TODO *)
+(* | Replace_pattern _ -> assert false (* TODO *) *)
| Rewrite _ -> assert false (* TODO *)
| Right _ -> current_size + 5
| Ring _ -> current_size + 4
(pretty_append
[Box.Text([],"with")]
t2)@where)
- | Change_pattern _ -> assert false (* TODO *)
+(* | Change_pattern _ -> assert false (* TODO *) *)
| Contradiction _ -> Box.Text([],"contradiction")
| Cut (_, term) ->
Box.V([],[Box.Text([],"cut");
Box.smallskip;
Box.Text([],"=")]);
Box.indent (ast2astBox term)])
- | Reduce _
- | ReduceAt _ -> assert false (* TODO *)
+(* | Reduce _ *)
+ | Reduce _ -> assert false (* TODO *)
| Reflexivity _ -> Box.Text([],"reflexivity")
| Replace (_, t1, t2) ->
Box.V([],
(pretty_append
[Box.Text([],"with")]
t2))
- | Replace_pattern _ -> assert false (* TODO *)
+(* | Replace_pattern _ -> assert false (* TODO *) *)
| Rewrite _ -> assert false (* TODO *)
| Right _ -> Box.Text([],"right")
| Ring _ -> Box.Text([],"ring")