- | Change_pattern (_, _, _) -> assert false (* TODO *)
- | Contradiction -> current_size + 13
- | Cut term -> countterm (current_size + 4) term
- | Decompose (ident, principles) ->
- List.fold_left
- (fun size s -> size + (String.length s))
- (current_size + 11 + String.length ident) principles
- | Discriminate ident -> current_size + 12 + (String.length ident)
- | Elim (term, using) ->
+*) assert false
+(* | Change_pattern _ -> assert false (* TODO *) *)
+ | Contradiction _ -> current_size + 13
+ | Cut (_, term) -> countterm (current_size + 4) term
+ | Decompose (_, term) ->
+ countterm (current_size + 11) term
+ | Discriminate (_, term) -> countterm (current_size + 12) term
+ | Elim (_, term, using) ->