+let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
+ let module C = Cic in
+ let module K = Content in
+ let rec aux =
+ function
+ [] -> [],[]
+ | t::l1 ->
+ let subproofs,args = aux l1 in
+ if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
+ let new_subproof =
+ acic2content
+ seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
+ let new_arg =
+ K.Premise
+ { K.premise_id = gen_id premise_prefix seed;
+ K.premise_xref = new_subproof.K.proof_id;
+ K.premise_binder = new_subproof.K.proof_name;
+ K.premise_n = None
+ } in
+ new_subproof::subproofs,new_arg::args
+ 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 premise_prefix seed;
+ K.premise_xref = idr;
+ K.premise_binder = Some b;
+ K.premise_n = Some n
+ }
+ else (K.Term t)
+ | C.AConst(id,uri,[]) ->
+ let sort =
+ (try Hashtbl.find ids_to_inner_sorts id
+ with Not_found -> "Type") in
+ if sort ="Prop" then
+ K.Lemma
+ { K.lemma_id = gen_id lemma_prefix seed;
+ K.lemma_name = UriManager.name_of_uri uri;
+ K.lemma_uri = UriManager.string_of_uri uri
+ }
+ else (K.Term t)
+ | C.AMutConstruct(id,uri,tyno,consno,[]) ->
+ let sort =
+ (try Hashtbl.find ids_to_inner_sorts id
+ with Not_found -> "Type") in
+ if sort ="Prop" then
+ let inductive_types =
+ (let o,_ =
+ CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ in
+ match o with
+ | Cic.InductiveDefinition (l,_,_,_) -> l
+ | _ -> assert false
+ ) in
+ let (_,_,_,constructors) =
+ List.nth inductive_types tyno in
+ let name,_ = List.nth constructors (consno - 1) in
+ K.Lemma
+ { K.lemma_id = gen_id lemma_prefix seed;
+ K.lemma_name = name;
+ K.lemma_uri =
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
+ ")"
+ }
+ else (K.Term t)
+ | _ -> (K.Term t)) in
+ subproofs,hd::args
+ in
+ match (aux l) with
+ [p],args ->
+ [{p with K.proof_name = None}],
+ List.map
+ (function
+ K.Premise prem when prem.K.premise_xref = p.K.proof_id ->
+ K.Premise {prem with K.premise_binder = None}
+ | i -> i) args
+ | p,a as c -> c
+
+and
+
+build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =