- nast_of_cic0 ~freshid ~output_type ~subst
- (nast_of_cic1 ~freshid ~output_type ~subst) ~context father_id term
- | Some (env, ctors, pid) ->
- let id, idref = freshid father_id in
- let idrefs =
- List.map
- (fun term ->
- let id, _ =
- freshid
- ~reference:
- (match term with NCic.Const nref -> nref | _ -> assert false)
- father_id
- in
- match id with Some id -> id | None -> assert false
- ) ctors in
- let env =
- List.map
- (fun (name, term) ->
- name,nast_of_cic1 ~freshid ~output_type ~subst ~context id term
- ) env in
- let _, symbol, args, _ =
- try
- TermAcicContent.find_level2_patterns32 pid
- with Not_found -> assert false in
- let ast = instantiate32 idrefs env symbol args in
+ nast_of_cic0 ~idref ~output_type ~subst
+ (nast_of_cic1 ~idref ~output_type ~subst) ~context term
+ | Some (env, ctors, pid) ->
+ let idrefs =
+ List.map
+ (fun term ->
+ let attrterm =
+ idref
+ ~reference:
+ (match term with NCic.Const nref -> nref | _ -> assert false)
+ (CicNotationPt.Ident ("dummy",None))
+ in
+ match attrterm with
+ Ast.AttributedTerm (`IdRef id, _) -> id
+ | _ -> assert false
+ ) ctors
+ in
+ let env =
+ List.map
+ (fun (name, term) ->
+ name,
+ nast_of_cic1 ~idref ~output_type ~subst ~context term
+ ) env
+ in
+ let _, symbol, args, _ =
+ try
+ TermAcicContent.find_level2_patterns32 pid
+ with Not_found -> assert false
+ in
+ let ast = instantiate32 idrefs env symbol args in