(* =================================== 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
;;
(* ========================= dispatching of auto/auto_paramod ============ *)
-let auto_tac ~params:(_,flags as params) =
+let auto_tac ~params:(_,flags as params) ?trace_ref =
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
NnAuto.fast_eq_check_tac ~params
else if List.mem_assoc "slir" flags then
- NnAuto.auto_tac ~params
+ NnAuto.auto_tac ~params ?trace_ref
else
auto_tac ~params
;;