X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=2404fbea3971fd2ffa99286fa53ff92bbd55f19a;hb=21bf57e0b7de37faa4991e136cf6f09cfbf4d0a3;hp=dfb742810c6d2525cd255443ebf517e7031129fe;hpb=c43f710f5e23e940114b1623329f650814e783af;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index dfb742810..2404fbea3 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -449,7 +449,7 @@ and proof2pres term2pres p =
     let module Con = Content in
     function
         Con.Aux n -> 
-          P.Mtext ([],"aux " ^ string_of_int n)
+          P.Mtext ([],"aux " ^ n)
       | Con.Premise prem -> 
           P.Mtext ([],"premise")
       | Con.Term t -> 
@@ -469,7 +469,7 @@ and proof2pres term2pres p =
      let inductive_arg,args_for_cases = 
        (match conclude.Con.conclude_args with
            Con.Aux(n)::_::tl ->
-             let l1,l2 = split n tl in
+             let l1,l2 = split (int_of_string n) tl in
              let last_pos = (List.length l2)-1 in
              List.nth l2 last_pos,l1
          | _ -> assert false) in