From 88efee4c688d660d2205c5933d302770acb5b407 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 18 Jan 2010 09:59:04 +0000 Subject: [PATCH] Invocation of paramod --- helm/software/components/ng_tactics/nAuto.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 5c5bb471b..ad9c155ca 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -1709,6 +1709,8 @@ let auto_tac ~params = let auto_tac ~params:(_,flags as params) = if List.mem_assoc "paramodulation" flags then auto_paramod_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 -- 2.39.2