- name,NCic.Def _ -> assert false
- | name,NCic.Decl (NCic.Const nref)
- | name,NCic.Decl (NCic.Appl (NCic.Const nref::_))
- when
- let NReference.Ref (uri',_) = nref in
- NUri.eq uri uri'
- ->
- let name = mk_id name in
- name, Some (
- CicNotationPt.Appl
- (rec_name ::
- params @
- [p_name] @
- k_names @
- List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @
- [name]))
- | name,_ -> mk_id name,None
+ _,NCic.Def _ -> assert false
+ | name,NCic.Decl ty ->
+ let context,ty = my_split_prods ~subst:[] [] (-1) ty in
+ match ty with
+ | NCic.Const nref
+ | NCic.Appl (NCic.Const nref::_)
+ when
+ let NReference.Ref (uri',_) = nref in
+ NUri.eq uri uri'
+ ->
+ let abs = List.rev_map (fun id,_ -> mk_id id) context in
+ let name = mk_id name in
+ name, Some (
+ List.fold_right
+ (fun id res ->
+ CicNotationPt.Binder (`Lambda,(id,None),res))
+ abs
+ (CicNotationPt.Appl
+ (rec_name ::
+ params @
+ [p_name] @
+ k_names @
+ List.map (fun _ -> CicNotationPt.Implicit)
+ (List.tl args) @
+ [CicNotationPt.Appl (name::abs)])))
+ | _ -> mk_id name,None