clears_note: string;
case: int list;
skip_thm_and_qed : bool;
- skip_initial_lambdas : bool;
}
(* helpers ******************************************************************)
(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
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]
| _ ->
(* 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;
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