From f8c1d3c7d0e1bdce57c763ca3602e88e00d4af9c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 3 Nov 2008 08:59:55 +0000 Subject: [PATCH] removed prerr_endline --- helm/software/components/tactics/auto.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 23909cddf..d191c436a 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -613,15 +613,12 @@ let new_metasenv_and_unify_and_t init_cache_and_tables ~dbd flags.use_library true true false universe (proof'''',newmeta) in - prerr_endline "chiamo given clause"; Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive max_int max_int flags.timeout with | None, _,_,_ -> raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) | Some (_,proof''''',_), active,passive,_ -> - prerr_endline "torno"; - proof''''', ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive -- 2.39.2