- | Change (_, t1, t2, where) ->
-(*
- let where =
- (match where with
- None -> []
- | Some ident ->
- [Box.Text([],"in");
- Box.smallskip;
- Box.Text([],ident)]) in
- Box.V([],
- (pretty_append
- [Box.Text([],"change")]
- t1)@
- (pretty_append
- [Box.Text([],"with")]
- t2)@where)
-*) assert false
-(* | Change_pattern _ -> assert false (* TODO *) *)
- | Contradiction _ -> Box.Text([],"contradiction")
- | Cut (_, term) ->
- Box.V([],[Box.Text([],"cut");