X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=b65d131e6a158f8af5d0ccfd495f1e2d96bb40b2;hb=424982ded255df68245241f56064202844ed1194;hp=2531620096f3a2ce1a65dae35a1c13faacbcf4a4;hpb=ea3b15fdedb39c72ae1b39f210917c6f38fc062d;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 253162009..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
@@ -447,13 +447,15 @@ let get_flavour ?flavour attrs =
       | Some fl -> fl
       | None    -> aux attrs
 
-let proc_obj ?flavour st = function
+let proc_obj ?flavour ?(info="") st = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
       begin match get_flavour ?flavour attrs with
          | 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 "tactics: %u\nnodes: %u" steps nodes in
+            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 ->
             [T.Statement (flavour, Some s, t, Some v, "")]
@@ -469,8 +471,8 @@ let proc_obj ?flavour st = function
 
 (* interface functions ******************************************************)
 
-let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-   ?flavour prefix anobj = 
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types 
+   ?info ?depth ?flavour prefix anobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -481,7 +483,7 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
    } in
    L.time_stamp "P : LEVEL 2  ";
    HLog.debug "Procedural: level 2 transformation";
-   let steps = proc_obj st ?flavour anobj in
+   let steps = proc_obj st ?flavour ?info anobj in
    L.time_stamp "P : RENDERING";
    HLog.debug "Procedural: grafite rendering";
    let r = List.rev (T.render_steps [] steps) in