X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=7a33d6266da45052fc2a16328d60f8dcbf5ce5b8;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=53c87673bd165861c97ffb4e2564773ef4930725;hpb=12f96bd48b460d06f9858a334ee7c52d6831712f;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 53c87673b..7a33d6266 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
@@ -1706,15 +1709,17 @@ let auto_tac ~params =
 ;;
 
 (* ========================= 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
 ;;