- hExtlib: new function "list_assoc_all"

[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 0eb8d8efbf9565e8ef64382587879c18e3b76589..c8168aa4795860700e75ac5d2b376214dd535abb 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -34,11 +34,11 @@ let tex_formatter = ref None
 (* interface functions ******************************************************)
 
 let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types 
-   ?info ?depth ?flavour prefix anobj = 
-   let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in
+   ?info params anobj = 
+   let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params [] in
    L.time_stamp "P : LEVEL 2  ";
    HLog.debug "Procedural: level 2 transformation";
-   let steps = P2.proc_obj st ?flavour ?info anobj in
+   let steps = P2.proc_obj st ?info anobj in
    let _ = match !tex_formatter with
       | None     -> ()
       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
@@ -48,9 +48,9 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
    let r = List.rev (T.render_steps [] steps) in
    L.time_stamp "P : DONE     "; r
 
-let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-   prefix context annterm = 
-   let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in
+let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
+   context annterm = 
+   let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context in
    HLog.debug "Procedural: level 2 transformation";
    let steps = P2.proc_proof st annterm in
    let _ = match !tex_formatter with