From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 22 Jul 2003 08:43:32 +0000 (+0000)
Subject: 1. Modificiations due to the change ot K.Aux
X-Git-Tag: LucaOK~45
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=21bf57e0b7de37faa4991e136cf6f09cfbf4d0a3

1. Modificiations due to the change ot K.Aux
2. Assert false on Lambda with no name removed. Who generates them?
---

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
diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index bb062f9cc..da6eb714a 100644
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -296,11 +296,12 @@ let acic2cexpr ids_to_inner_sorts t =
              Binder (Some id,binder,decl,acic2cexpr t)) 
     | C.ACast (id,v,t) -> acic2cexpr v
     | C.ALambda (id,n,s,t) ->
-        (match n with
-           Cic.Anonymous -> assert false
-         | Cic.Name name ->
-             let decl = (name, acic2cexpr s) in 
-             Binder (Some id,"Lambda",decl,acic2cexpr t))
+        let name =
+          (match n with
+             Cic.Anonymous -> "_"
+           | Cic.Name name -> name) in
+        let decl = (name, acic2cexpr s) in 
+        Binder (Some id,"Lambda",decl,acic2cexpr t)
     | C.ALetIn (id,n,s,t) ->
         (match n with
            Cic.Anonymous -> assert false