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