let module C2A = Cic2acic in
let module K = Content in
{ K.proof_name = name;
- K.proof_id = proof_prefix ^ id ;
+ K.proof_id = gen_id proof_prefix seed ;
K.proof_context = [] ;
K.proof_apply_context = [];
K.proof_conclude =
let module C = Cic in
let module K = Content in
{ K.proof_name = name;
- K.proof_id = proof_prefix ^ id ;
+ K.proof_id = gen_id proof_prefix seed ;
K.proof_context = [] ;
K.proof_apply_context = [];
K.proof_conclude =
if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or
uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists"
else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd"
+ else if uri_str = "cic:/Coq/Init/Logic/False_ind.con" then "FalseInd"
else "ByInduction" in
let prefix = String.sub uri_str 0 n in
let ind_str = (prefix ^ ".ind") in
let p,a = split (n-1) (List.tl l) in
((List.hd l::p),a) in
let params_and_IP,tail_args = split (noparams+1) args in
- if method_name = "Exists" then
- (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args));
- prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args)));
let constructors =
(match inductive_types with
[(_,_,_,l)] -> l
let context' =
List.map
(function
- (id,None) as item -> item
+ (id,None) -> None
| (id,Some (name,Cic.ADecl t)) ->
- id,
- Some
- (* We should call build_decl_item, but we have not computed *)
- (* the inner-types ==> we always produce a declaration *)
- (`Declaration
- { K.dec_name = name_of name;
- K.dec_id = gen_id declaration_prefix seed;
- K.dec_inductive = false;
- K.dec_aref = get_id t;
- K.dec_type = t
- })
+ Some
+ (* We should call build_decl_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Declaration
+ { K.dec_name = name_of name;
+ K.dec_id = gen_id declaration_prefix seed;
+ K.dec_inductive = false;
+ K.dec_aref = get_id t;
+ K.dec_type = t
+ })
| (id,Some (name,Cic.ADef t)) ->
- id,
- Some
- (* We should call build_def_item, but we have not computed *)
- (* the inner-types ==> we always produce a declaration *)
- (`Definition
- { K.def_name = name_of name;
- K.def_id = gen_id definition_prefix seed;
- K.def_aref = get_id t;
- K.def_term = t
- })
+ Some
+ (* We should call build_def_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Definition
+ { K.def_name = name_of name;
+ K.def_id = gen_id definition_prefix seed;
+ K.def_aref = get_id t;
+ K.def_term = t
+ })
) context
in
(id,n,context',ty)