- Procedural convertible rewrites in the conclusion are now detected and replaced...

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 4ce01707cd9d32431f160c1bd28a1f67b6ca05d6..68c88496ba91fbfe3e735a0264f2eb9be266b166 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -63,8 +63,12 @@ let proc_obj ?(info="") proc_proof sorts params context = function
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof v in
             let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
-            let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
-              "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+            let text =
+              if List.mem G.IPComments params then 
+                 Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+                 "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+              else
+                 ""
            in
             T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
          | flavour when List.mem flavour def_flavours ->