From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 22 Oct 2008 19:25:24 +0000 (+0000)
Subject: we aligned the implementation to the plmms08 paper
X-Git-Tag: make_still_working~4644
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04c05cf08605156ba8c6fa7225b4a90496c03698;p=helm.git

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 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 ->
diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 8d1108abe..52192f723 100644
--- 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