From 0be569e573dcad311bcd55212fd3fcf2c37be0ff Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 May 2007 11:37:10 +0000 Subject: [PATCH] some minor fixes done in cividale (bugfix coming from andrea's branch) --- helm/software/components/tactics/auto.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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")) ;; -- 2.39.2