we aligned the implementation to the plmms08 paper

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 ->

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 8d1108abe1dda13b1532a0356a387b97ba40cc1c..52192f723de1f0181a3f0cb1474307de068dc025 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -52,7 +52,7 @@ type status = {
 
 let info st str = {st with info = st.info ^ str ^ "\n"}
 
-let defined_premise = "DEFINED"
+let defined_premise = "LOCAL"
 
 let define c v =
    let name = C.Name defined_premise in