X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=da6eb714ad5087544edc87a787395e697fe8f46d;hb=21bf57e0b7de37faa4991e136cf6f09cfbf4d0a3;hp=bb062f9cc2cce1337e038ce6cb33dc4df687c930;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git

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