...

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 23b934d51d35fc151f0833f2e518838c820a59ac..b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/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 ******************************************************************)
@@ -199,7 +198,10 @@ let mk_convert st ?name sty ety note =
    let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
       note (Pp.ppterm csty) (Pp.ppterm cety)
    in
+   assert (Ut.is_sober csty); 
+   assert (Ut.is_sober cety);
    if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
+   let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
       | None         -> [T.Change (sty, ety, None, e, ""(*note*))]
       | Some (id, i) -> 
@@ -267,7 +269,7 @@ let mk_rewrite st dtext where qs tl direction t =
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (H.cic t) in
    let dno = dno && match get_inner_types st t with
-      | None          -> true
+      | None          -> false
       | Some (it, et) -> 
          DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
    in
@@ -293,7 +295,8 @@ and proc_letin st what name v t =
                  mk_fwd_rewrite st dtext intro tl false v
               | v                                                     ->
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
-                 st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+                 let ity = H.acic_bc st.context ity in
+                 st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
            st, C.Decl (H.cic ity), rqv
         | None          ->
@@ -376,12 +379,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 +427,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 +435,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 +448,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