Debugging code fixed. To enable debugging just set debug to true at the

top of the file.

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 59e90e6daec19d7aaa6c9e2b4c27f7f61c86feda..aca89bd4a609a8b427aaa71fc4f8200786fc81b5 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -28,7 +28,7 @@ open AutoCache;;
 
 let debug = false;;
 let debug_print s = 
-  if debug then () else prerr_endline (Lazy.force s);;
+  if debug then prerr_endline (Lazy.force s);;
 
 (* functions for retrieving theorems *)