- (function (i,canonical_context,term) ->
- let acanonical_context =
- let rec aux =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- let at =
- acic_term_of_cic_term_context' conjectures tl t
- in
- Some (n,C.ADecl at)::(aux tl)
- | (Some (n,C.Def t))::tl ->
- let at =
- acic_term_of_cic_term_context' conjectures tl t
- in
- Some (n,C.ADef at)::(aux tl)
- | None::tl -> None::(aux tl)
- in
- aux canonical_context
- in
- let aterm =
- acic_term_of_cic_term_context' conjectures canonical_context term
+ (function (i,canonical_context,term) as conjecture ->
+ let cid = "c" ^ string_of_int !conjectures_seed in
+ Hashtbl.add ids_to_conjectures cid conjecture ;
+ incr conjectures_seed ;
+ let acanonical_context =
+ let rec aux =
+ function
+ [] -> []
+ | hyp::tl ->
+ let hid = "h" ^ string_of_int !hypotheses_seed in
+ Hashtbl.add ids_to_hypotheses hid hyp ;
+ incr hypotheses_seed ;
+ match hyp with
+ (Some (n,C.Decl t)) ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ (hid,Some (n,C.ADecl at))::(aux tl)
+ | (Some (n,C.Def t)) ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ (hid,Some (n,C.ADef at))::(aux tl)
+ | None -> (hid,None)::(aux tl)
+ in
+ aux canonical_context