we aligned the implementation to the plmms08 paper

[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 c9a3232484b30b60378dfc0da9b49bdd18996466..b65d131e6a158f8af5d0ccfd495f1e2d96bb40b2 100644 (file)
--- 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 ->