X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_procedural%2FproceduralTypes.ml;h=53605271d5627154a1227afd782b2aa577eb9e36;hb=e55c40ddebaa3664f294a8dd8df162e8c1fa5020;hp=95fdc6e562d6c8e281c937509dd8b57d57431ab9;hpb=68d46ac40a575f3fce5958fb2776b38739703951;p=helm.git

diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index 95fdc6e56..53605271d 100644
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -164,7 +164,7 @@ let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
 let rec render_step sep a = function
    | Note s               -> mk_note s :: a
    | Theorem (n, t, s)    -> mk_note s :: mk_theorem n t :: a 
-   | Qed s                -> mk_note s :: mk_qed :: a
+   | Qed s                -> (* mk_note s :: *) mk_qed :: a
    | Id s                 -> mk_note s :: cont sep (mk_id :: a)
    | Intros (c, ns, s)    -> mk_note s :: cont sep (mk_intros c ns :: a)
    | Cut (n, t, s)        -> mk_note s :: cont sep (mk_cut n t :: a)