X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=6f49f7d36575b4c9d21cf9e66a768728d1bcda0d;hb=668fb315dc8502dc1b4d336eba19ab9436bf5b7a;hp=5c5bb471b7d3c30c1f19ca8712d859eaa56fd098;hpb=21ee96d317a4f0e7abfe76f697defe78acc10b94;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 5c5bb471b..6f49f7d36 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -24,6 +24,9 @@ module Ast = CicNotationPt
 
 (* =================================== 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
@@ -1675,7 +1678,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 +1712,10 @@ 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 "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