more informations on nodes, fixed a bug on conversion, we use ; instead of . whenever...

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 4ccb78ace32522efbd43d8b9706bbe7f81deca71..3ee088696db48a6bc58eb67372214132f5df906c 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -215,16 +215,16 @@ let get_intro = function
    | C.Anonymous -> None
    | C.Name s    -> Some s
 
-let mk_intros st script =
+let mk_intros st what script =
    let intros st script =
       if st.intros = [] then script else
       let count = List.length st.intros in
       T.Intros (Some count, List.rev st.intros, "") :: script
    in
    let clears st script =
-      if st.clears = [] then script else T.Clear (st.clears, st.clears_note) :: script
+      if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
    in
-   intros st (clears st script)   
+   intros st (clears st (convert st what @ script))   
 
 let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
@@ -289,18 +289,18 @@ and proc_letin st what name v t =
    else
       [T.Apply (what, dtext)]
    in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_rel st what = 
    let _, dtext = test_depth st in
    let text = "assumption" in
    let script = [T.Apply (what, dtext ^ text)] in 
-   mk_intros st script
+   mk_intros st what script
 
 and proc_mutconstruct st what = 
    let _, dtext = test_depth st in
    let script = [T.Apply (what, dtext)] in 
-   mk_intros st script   
+   mk_intros st what script   
 
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
@@ -320,7 +320,7 @@ and proc_appl st what hd tl =
       in
       let synth = mk_synth I.S.empty decurry in
       let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
-      let script = List.rev (mk_arg st hd) @ convert st what in
+      let script = List.rev (mk_arg st hd) in
       match rc with
          | Some (i, j, uri, tyno) ->
            let classes, tl, _, where = split2_last classes tl in
@@ -345,12 +345,12 @@ and proc_appl st what hd tl =
    else
       [T.Apply (what, dtext)]
    in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_other st what =
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
    let script = [T.Note text] in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_proof st t = 
    let f st =