let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
?info ?depth ?flavour prefix anobj =
let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
?info ?depth ?flavour prefix anobj =
- let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in
- L.time_stamp "P : LEVEL 1 ";
- HLog.debug "Procedural: level 1 transformation";
- let steps = P1.proc_obj st ?flavour ?info anobj in
+ let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in
+ L.time_stamp "P : LEVEL 2 ";
+ HLog.debug "Procedural: level 2 transformation";
+ let steps = P2.proc_obj st ?flavour ?info anobj in
- let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in
- HLog.debug "Procedural: level 1 transformation";
- let steps = P1.proc_proof st annterm in
+ let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in
+ HLog.debug "Procedural: level 2 transformation";
+ let steps = P2.proc_proof st annterm in