- 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
+ 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