-(*
-let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
- let module C = Cic in
- let module K = Content in
- let rec aux l subproofs =
- match l with
- [] -> []
- | t::l1 ->
- if (test_for_lifting t ~ids_to_inner_types) then
- (match subproofs with
- [] -> assert false
- | p::tl ->
- let new_arg =
- K.Premise
- { K.premise_id = gen_id seed;
- K.premise_xref = p.K.proof_id;
- K.premise_binder = p.K.proof_name;
- K.premise_n = None
- }
- in new_arg::(aux l1 tl))
- else
- let hd =
- (match t with
- C.ARel (idr,idref,n,b) ->
- let sort =
- (try Hashtbl.find ids_to_inner_sorts idr
- with Not_found -> "Type") in
- if sort ="Prop" then
- K.Premise
- { K.premise_id = gen_id seed;
- K.premise_xref = idr;
- K.premise_binder = Some b;
- K.premise_n = Some n
- }
- else (K.Term t)
- | _ -> (K.Term t)) in
- hd::(aux l1 subproofs)
- in aux l subproofs
-;;
-*)
-