| Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
| Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
| Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[]
+ | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[]
(* calculate depth in the univ_graph*)
| Cic.Appl l ->
let l, fixpoints =
assert(fixpoints_ty = []);
NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
fixpoints_bo @ fixpoints_ty
- | Cic.InductiveDefinition (_,_,_,_) -> assert false (*
+ | Cic.InductiveDefinition (itl,_,leftno,_) ->
let ind = let _,x,_,_ = List.hd itl in x in
- let itl =
- List.map
- (fun name, _, ty, cl ->
- [], name, convert_term ty,
- List.map (fun name, ty -> [], name, convert_term ty) cl)
- itl
+ let itl, fix_itl =
+ List.fold_right
+ (fun (name, _, ty, cl) (itl,acc) ->
+ let ty, fix_ty = convert_term uri ty in
+ let cl, fix_cl =
+ List.fold_right
+ (fun (name, ty) (cl,acc) ->
+ let ty, fix_ty = convert_term uri ty in
+ ([], name, ty)::cl, acc @ fix_ty)
+ cl ([],[])
+ in
+ ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
+ itl ([],[])
in
- NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) *)
+ NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)),
+ fix_itl
| Cic.Variable _
| Cic.CurrentProof _ -> assert false
;;