Added an implicit parameter to branch_tac to allow branching on a

[helm.git] / helm / software / components / ng_tactics / nAuto.ml

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 5c5bb471b7d3c30c1f19ca8712d859eaa56fd098..53c87673bd165861c97ffb4e2564773ef4930725 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1675,7 +1675,7 @@ let group_by_tac ~eq_predicate ~action:tactic status =
     let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in
     List.map (fun x -> List.assoc x l2) l1
   in
-  NTactics.block_tac ([ NTactics.branch_tac ]
+  NTactics.block_tac ([ NTactics.branch_tac ~force:false]
     @
     HExtlib.list_concat ~sep:[NTactics.shift_tac]
       (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes)
@@ -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