X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=698053b40d48fff8c92823522f6aec05056abdf5;hb=004ccf29097c8ab5c4997555b54aba5831fa035a;hp=06aa8b303496b17942cc7e62d774ce510617bb88;hpb=61f3a8a688132be943b81befa5805e27148f2038;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 06aa8b303..698053b40 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -933,9 +933,11 @@ let int params name default =
 let flags_of_params params ?(for_applyS=false) () =
  let int = int params in
  let bool = bool params in
+ let close_more = bool "close_more" false in
  let use_paramod = bool "use_paramod" true in
  let use_only_paramod =
   if for_applyS then true else bool "paramodulation" false in
+ let use_library = bool "library" (not use_only_paramod) in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in
@@ -948,9 +950,11 @@ let flags_of_params params ?(for_applyS=false) () =
        else
          infinity
       else
-       Unix.gettimeofday() +. (float_of_int timeout); 
+       Unix.gettimeofday() +. (float_of_int timeout);
+    AutoTypes.use_library = use_library; 
     AutoTypes.use_paramod = use_paramod;
     AutoTypes.use_only_paramod = use_only_paramod;
+    AutoTypes.close_more = close_more;
     AutoTypes.dont_cache_failures = false;
   }
 
@@ -1111,11 +1115,14 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
-      let use_library = not flags.use_only_paramod in
+      let use_library = flags.use_library in
       let tables,cache,newmeta =
 	init_cache_and_tables dbd use_library (proof, goal) in
       let tables,cache,newmeta =
-	close_more tables newmeta context (proof, goal) auto_all_solutions cache in
+        if flags.close_more then
+	  close_more 
+	    tables newmeta context (proof, goal) auto_all_solutions cache 
+	else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
       let (_,oldmetasenv,_,_) = proof in
       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in