K.inductive_type = ty;
K.inductive_constructors = build_constructors seed cl
}
+in
+let build_fixpoint b seed =
+ fun (_,n,_,ty,t) ->
+ let t = nast_of_cic ~context:[] t in
+ let ty = nast_of_cic ~context:[] ty in
+ `Definition
+ { K.def_id = gen_id inductive_prefix seed;
+ K.def_name = Some n;
+ K.def_aref = "";
+ K.def_type = ty;
+ K.def_term = t;
+ }
in
let res =
match kind with
- | NCic.Fixpoint (is_rec, ifl, _) -> assert false
+ | 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 = `Inductive lno;
+ 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,_) ->