open Ast2pres
open TacticAst
-let count_pattern current_size p =
+let count_pattern current_size (wanted,hyps_pat,concl_pat) =
if current_size > maxsize then current_size
else
-assert false
+ let size = countterm (current_size + 3) concl_pat in
+ let size =
+ List.fold_left
+ (fun s (id,t) -> countterm (s + String.length id + 1) t) size hyps_pat in
+ match wanted with
+ None -> size + 3
+ | Some t -> countterm (size + 9) t
let count_kind =
function