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 25f4e0fc70ff52c85f4e49f7630605fcae456bcc..53c87673bd165861c97ffb4e2564773ef4930725 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -41,7 +41,7 @@ let auto_paramod ~params:(l,_) status goal =
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
   | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
+  | (pt, _, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;
@@ -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