From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 May 2007 11:37:10 +0000 (+0000)
Subject: some minor fixes done in cividale (bugfix coming from andrea's branch)
X-Git-Tag: make_still_working~6346
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0be569e573dcad311bcd55212fd3fcf2c37be0ff;p=helm.git

some minor fixes done in cividale (bugfix coming from andrea's branch)
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index c7cffc8af..f767ed21e 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,7 +26,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug = true;;
+let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
@@ -796,11 +796,9 @@ let rec auto_main tables maxm context flags elems universe cache =
           debug_print (lazy (AutoCache.cache_print context cache));
           if sort = T (* && tl <> []*)  then 
           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
-	  (* Success (metasenv,subst,tl), tables, cache,maxm *)
-          (*
             (debug_print 
 	       (lazy (" FAILURE(not in prop)"));
-            aux flags tables maxm cache tl (* FAILURE (not in prop) *)) *)
+            aux flags tables maxm cache ((metasenv,subst,gl)::tl))
           else
           match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
           | Fail s, tables, cache, maxm' -> 
@@ -947,7 +945,9 @@ let auto flags metasenv tables universe cache context metasenv gl =
   | Success (metasenv,subst,_), tables,cache,_ -> 
       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
       Some (subst,metasenv), cache
-  | Fail s,tables,cache,maxm -> None,cache
+  | Fail s,tables,cache,maxm -> 
+      prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+      None,cache
 ;;
 
 let bool params name default =
@@ -1185,6 +1185,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
             in
               proof,opened
 	| Fail s,tables,cache,maxm -> 
+	    prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
 	    raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 ;;