+ | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
+ (match target with
+ C.Rel n ->
+ (match kind with
+ `Recursive l ->
+ let funs =
+ List.map2
+ (fun n bo ->
+ match bo with
+ `Proof bo ->
+ (match
+ bo.Con.proof_conclude.Con.conclude_conclusion,
+ bo.Con.proof_name
+ with
+ Some ty, Some name ->
+ (name,n,term2cic ty,proof2cic premise_env bo)
+ | _,_ -> assert false)
+ | _ -> assert false)
+ l defs in
+ C.Fix (n, funs)
+ | `CoRecursive ->
+ let funs =
+ List.map
+ (function bo ->
+ match bo with
+ `Proof bo ->
+ (match
+ bo.Con.proof_conclude.Con.conclude_conclusion,
+ bo.Con.proof_name
+ with
+ Some ty, Some name ->
+ (name,term2cic ty,proof2cic premise_env bo)
+ | _,_ -> assert false)
+ | _ -> assert false)
+ defs in
+ C.CoFix (n, funs)
+ | _ -> (* no inductive types in local contexts *)
+ assert false)
+ | _ -> assert false)