hacks for paramodulation declarative proofs

[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 23b934d51d35fc151f0833f2e518838c820a59ac..f39aa18bd96ee3a162baa10fa6da07ca3b6f8805 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -56,7 +56,6 @@ type status = {
    clears_note: string;
    case: int list;
    skip_thm_and_qed : bool;
-   skip_initial_lambdas : bool;
 }
 
 (* helpers ******************************************************************)
@@ -376,12 +375,7 @@ and proc_proof st t =
          (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) 
          | None          -> None, "\nNo types"
       in
-      let context, clears = 
-        if st.skip_initial_lambdas then
-          st.context, []
-        else
-          Cn.get_clears st.context (H.cic t) xtypes 
-      in
+      let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
       let note = Pp.ppcontext st.context ^ note in
       {st with context = context; clears = clears; clears_note = note; }
    in
@@ -429,13 +423,6 @@ let proc_obj st = function
       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 "tactics: %u\nnodes: %u" steps nodes in
-      let ast = 
-        if st.skip_initial_lambdas then 
-          match ast with
-            | T.Intros _::tl -> tl
-            | ast -> ast
-        else ast
-      in
       if st.skip_thm_and_qed then ast
       else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
@@ -444,7 +431,7 @@ let proc_obj st = function
 (* interface functions ******************************************************)
 
 let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-?(skip_thm_and_qed=false) ?(skip_initial_lambdas=false) prefix aobj = 
+?(skip_thm_and_qed=false) prefix aobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -457,7 +444,6 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       clears_note = "";
       case        = [];
       skip_thm_and_qed = skip_thm_and_qed;
-      skip_initial_lambdas = skip_initial_lambdas;
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in