- let status = ref status in
- for i = 0 to n-1 do
- if sort_of !status [] ti.(i) <> InProp then begin
- let status',e,t = extract_std_constant !status vkn.(i) ci.(i) ti.(i) in
- status := status';
- terms.(i) <- e;
- types.(i) <- t;
- end
- done;
- let status = !status in
+ let status,res = array_mapi_status status
+ (fun status i _ ->
+ let _,head = split_all_prods status ~subst:[] [] ti.(i) in
+ match head with
+ NCic.Sort s when classify_sort s = InProp -> status,`None
+ | NCic.Sort _ ->
+ let n = type_scheme_nb_args status [] ti.(i) in
+ let ids = iterate (fun l -> anonymous_name::l) n [] in
+ status,`Type (Dtype (vkn.(i), ids, Tunknown))
+ | _ ->
+ if sort_of status [] ti.(i) <> InProp then
+ let status,e,t = extract_std_constant status vkn.(i) ci.(i) ti.(i) in
+ status,`Some (e,t)
+ else
+ status,`None
+ ) ti in
+ let axioms,terms,types =
+ Array.fold_right
+ (fun x ((axioms,terms,types) as res) ->
+ match x with
+ `None -> res
+ | `Some (t,ty) -> axioms,t::terms,ty::types
+ | `Type decl -> decl::axioms,terms,types
+ ) res ([],[],[]) in