From 36dd8daeea2b685837d27e84ca204548d8d280fd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jun 2007 13:02:02 +0000 Subject: [PATCH] auto proof are printed in procedural style --- helm/software/matita/matitaScript.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index e446b67f5..a615e6f9f 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/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