let ids_to_hypotheses = Hashtbl.create 23 in
let hypotheses_seed = ref 0 in
let seed = ref 1 in (* 'i0' is used for the whole sequent *)
+ let sequent =
+ let i,canonical_context,term = sequent in
+ let canonical_context' =
+ List.fold_right
+ (fun d canonical_context' ->
+ let d' =
+ match d with
+ None -> None
+ | Some (n, Cic.Decl t)->
+ Some (n, Cic.Decl (Unshare.unshare t))
+ | Some (n, Cic.Def (t,None)) ->
+ Some (n,
+ Cic.Def ((Unshare.unshare t),None))
+ | Some (_,Cic.Def (_,Some _)) -> assert false
+ in
+ d::canonical_context'
+ ) [] canonical_context
+ in
+ let term' = Unshare.unshare term in
+ (i,canonical_context',term')
+ in
let (metano,acontext,agoal) =
aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
= aconjecture_of_conjecture' conjectures conjecture in
(cid,i,acanonical_context,aterm))
conjectures' in
-(* let idrefs',revacanonical_context =
- let rec aux context idrefs =
- function
- [] -> idrefs,[]
- | hyp::tl ->
- let hid = "h" ^ string_of_int !hypotheses_seed in
- let new_idrefs = hid::idrefs in
- xxx_add ids_to_hypotheses hid hyp ;
- incr hypotheses_seed ;
- match hyp with
- (Some (n,C.Decl t)) ->
- let final_idrefs,atl =
- aux (hyp::context) new_idrefs tl in
- let at =
- acic_term_of_cic_term_context'
- conjectures context idrefs t None
- in
- final_idrefs,(hid,Some (n,C.ADecl at))::atl
- | (Some (n,C.Def (t,_))) ->
- let final_idrefs,atl =
- aux (hyp::context) new_idrefs tl in
- let at =
- acic_term_of_cic_term_context'
- conjectures context idrefs t None
- in
- final_idrefs,(hid,Some (n,C.ADef at))::atl
- | None ->
- let final_idrefs,atl =
- aux (hyp::context) new_idrefs tl
- in
- final_idrefs,(hid,None)::atl
- in
- aux [] [] (List.rev canonical_context)
- in
- let aterm =
- acic_term_of_cic_term_context' conjectures
- canonical_context idrefs' term None
- in
- (cid,i,(List.rev revacanonical_context),aterm)
- ) conjectures' in *)
(* let time1 = Sys.time () in *)
let bo' = eta_fix conjectures' [] bo in
let ty' = eta_fix conjectures' [] ty in