- let res =
- match kind with
- | NCic.Fixpoint (is_rec, ifl, _) ->
- (gen_id object_prefix seed, conjectures,
- `Joint
- { K.joint_id = gen_id joint_prefix seed;
- K.joint_kind =
- if is_rec then
- `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl)
- else `CoRecursive;
- K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
- })
- | NCic.Inductive (is_ind, lno, itl, _) ->
- (gen_id object_prefix seed, conjectures,
- `Joint
- { K.joint_id = gen_id joint_prefix seed;
- K.joint_kind =
- if is_ind then `Inductive lno else `CoInductive lno;
- K.joint_defs = List.map (build_inductive is_ind seed) itl
- })
- | NCic.Constant (_,_,Some bo,ty,_) ->
- let ty = nast_of_cic ~context:[] ty in
- let bo = nast_of_cic ~context:[] bo in
- (gen_id object_prefix seed, conjectures,
- `Def (K.Const,ty,
- build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
- | NCic.Constant (_,_,None,ty,_) ->
- let ty = nast_of_cic ~context:[] ty in
- (gen_id object_prefix seed, conjectures,
- `Decl (K.Const,
- (*CSC: ??? get_id ty here used to be the id of the axiom! *)
- build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))
- in
- res,ids_to_refs
+ match kind with
+ | NCic.Fixpoint (is_rec, ifl, _) ->
+ (gen_id object_prefix seed, conjectures,
+ `Joint
+ { K.joint_id = gen_id joint_prefix seed;
+ K.joint_kind =
+ if is_rec then
+ `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl)
+ else `CoRecursive;
+ K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
+ })
+ | NCic.Inductive (is_ind, lno, itl, _) ->
+ (gen_id object_prefix seed, conjectures,
+ `Joint
+ { K.joint_id = gen_id joint_prefix seed;
+ K.joint_kind =
+ if is_ind then `Inductive lno else `CoInductive lno;
+ K.joint_defs = List.map (build_inductive is_ind seed) itl
+ })
+ | NCic.Constant (_,_,Some bo,ty,_) ->
+ let ty = nast_of_cic ~context:[] ty in
+ let bo = nast_of_cic ~context:[] bo in
+ (gen_id object_prefix seed, conjectures,
+ `Def (K.Const,ty,
+ build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
+ | NCic.Constant (_,_,None,ty,_) ->
+ let ty = nast_of_cic ~context:[] ty in
+ (gen_id object_prefix seed, conjectures,
+ `Decl (K.Const,
+ (*CSC: ??? get_id ty here used to be the id of the axiom! *)
+ build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))
+;;
+
+let with_idrefs foo status obj =
+ let ids_to_refs = Hashtbl.create 211 in
+ let register_ref = Hashtbl.add ids_to_refs in
+ foo status ~idref:(idref register_ref) obj, ids_to_refs