X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=b65d131e6a158f8af5d0ccfd495f1e2d96bb40b2;hb=b615d727f53aaa868f28dd3ba16c988d79e61bba;hp=c9a3232484b30b60378dfc0da9b49bdd18996466;hpb=9e010764b6de0d8a268a6ecb83e8e90246bee129;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index c9a323248..b65d131e6 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -176,7 +176,7 @@ let get_type msg st t = H.get_type msg st.context (H.cic t)
 
 (* proof construction *******************************************************)
 
-let anonymous_premise = C.Name "PREMISE"
+let anonymous_premise = C.Name "UNNAMED"
 
 let mk_exp_args hd tl classes synth =
    let meta id = C.AImplicit (id, None) in
@@ -256,7 +256,7 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
 	    let ity = H.acic_bc st.context ity in
 	    let br1 = [T.Id ""] in
 	    let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
-	    let text = "non linear rewrite" in
+	    let text = "non-linear rewrite" in
 	    st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
 	 end
       | _                         -> assert false
@@ -453,8 +453,8 @@ let proc_obj ?flavour ?(info="") st = function
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof st 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"
-	       "COMMENTS" info "tactics" steps "nodes" nodes
+            let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+	       "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
 	    in
             T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
          | flavour when List.mem flavour def_flavours ->