applyTransformation: added debugging information

[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 9815580b6444ef8bb31669e0fd60aaae5cebb60b..d54130a0cd75fdac58377ec0a4920660aa921852 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -249,7 +249,7 @@ let mk_fwd_rewrite st dtext name tl direction t =
    match where with
       | C.ARel (_, _, i, premise) as v ->
          let where = Some (premise, name) in
-         let _script = convert_elim st ~name:(premise, i) t v e in 
+(*         let _script = convert_elim st ~name:(premise, i) t v e in *) 
          let script = mk_arg st what @ mk_arg st v (* @ script *) in
         let st = {st with context = Cn.clear st.context premise} in 
         st, T.Rewrite (direction, what, where, e, dtext) :: script
@@ -259,7 +259,7 @@ let mk_rewrite st dtext where qs tl direction t =
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
-   let script = convert_elim st t t e in
+   let script = [] (* convert_elim st t t e *) in
    script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
 
 let rec proc_lambda st name v t =
@@ -350,7 +350,7 @@ and proc_appl st what hd tl =
               let predicate = List.nth tl (parsno - i) in
                let e = Cn.mk_pattern j predicate in
               let using = Some hd in
-              convert_elim st what what e @ script @ 
+              (* convert_elim st what what e @ *) script @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
            let qs = proc_bkd_proofs (next st) synth [] classes tl in