From c9f6dcb0f6036e69548db1f991c4eab792321590 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 4 Jun 2007 13:02:02 +0000
Subject: [PATCH] auto proof are printed in procedural style

---
 matita/matitaScript.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index e446b67f5..a615e6f9f 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -548,7 +548,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
             Auto.revision time size depth
         in
         let proof_script = 
-          if true (* List.exists (fun (s,_) -> s = "paramodulation") params *) then
+          if List.exists (fun (s,_) -> s = "paramodulation") params then
               let proof_term = 
                 Auto.lambda_close ~prefix_name:"orrible_hack_" 
                   proof_term menv cc 
-- 
2.39.2