(* =================================== paramod =========================== *)
let auto_paramod ~params:(l,_) status goal =
+ let l = match l with
+ | None -> raise (Error (lazy "no proof found",None))
+ | Some l -> l in
let gty = get_goalty status goal in
let n,h,metasenv,subst,o = status#obj in
let status,t = term_of_cic_term status gty (ctx_of gty) in
let auto_tac ~params:(_,flags as params) =
if List.mem_assoc "paramodulation" flags then
auto_paramod_tac ~params
+ else if List.mem_assoc "demod" flags then
+ NnAuto.demod_tac ~params
else if List.mem_assoc "paramod" flags then
NnAuto.paramod_tac ~params
else if List.mem_assoc "fast_paramod" flags then