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
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 =