Procedural: we corrected two errors about the handling of mutcase (the "cases"

[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 f749ce8d287eb3046f771b415c54ea42145bb6b5..0eb8d8efbf9565e8ef64382587879c18e3b76589 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -26,7 +26,7 @@
 module L    = Librarian
 
 module T  = ProceduralTypes
-module P1 = Procedural1
+module P2 = Procedural2
 module X  = ProceduralTeX
 
 let tex_formatter = ref None
@@ -35,10 +35,10 @@ let tex_formatter = ref None
 
 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 _ = match !tex_formatter with
       | None     -> ()
       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
@@ -50,9 +50,9 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
 
 let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
    prefix context annterm = 
-   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
    let _ = match !tex_formatter with
       | None     -> ()
       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps