Hashtbl.add ids_to_hypotheses hid binding ;
incr hypotheses_seed ;
match binding with
- Some (n,Cic.Def (t,None)) ->
+ Some (n,Cic.Def (t,_)) ->
let acic = acic_of_cic_context context idrefs t None in
(binding::context),
((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
| None ->
(* Invariant: "" is never looked up *)
(None::context),((hid,None)::acontext),""::idrefs
- | Some (_,Cic.Def (_,Some _)) -> assert false
) context ([],[],[])
)
in
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 unsh_sequent =
let i,canonical_context,term = sequent in
let canonical_context' =
List.fold_right
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
+ | Some (n,Cic.Def (bo,Some ty)) ->
+ Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
in
d::canonical_context'
) canonical_context []
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
- metasenv sequent in
- ("i0",metano,acontext,agoal),
- ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
+ metasenv unsh_sequent in
+ (unsh_sequent,
+ (("i0",metano,acontext,agoal),
+ ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
;;
let acic_object_of_cic_object ?(eta_fix=true) obj =