| Some uri -> uri
in
let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
- let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let uri = baseuri_of_term termty in
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let (_,_,typeno,_) =
match termty with
C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
let parameters_tys =
(List.map
(fun t -> (
- match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with
+ match (T.type_of_aux' metasenv context t CicUniv.oblivion_ugraph) with
(term,graph) -> term))
parameters)
in
(*DEBUG*) debug_print (lazy ("private inversion: term before refinement: " ^
CicPp.ppterm t));
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
(*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: "
^ CicPp.ppterm ref_t));
(*DEBUG*) debug_print (lazy ("inversion begins"));
let _,metasenv,_subst,_,_, _ = proof in
let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
- let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let uri, typeno =
match termty with
| Cic.MutInd (uri,typeno,_)
| _ -> assert false
in
(* let uri = baseuri_of_term termty in *)
- let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let name,nleft,arity,cons_list =
match obj with
Cic.InductiveDefinition (tys,_,nleft,_) ->
for n = 1 to arity_consno do
a := (Cic.Implicit None)::(!a)
done;
- (* apply i_inv ? ...? H). *)
- Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
+ (* apply i_inv ? ...? H). *)
+ Cic.Appl ([Cic.Const(uri,[])] @ !a @ [term])
in
let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
let (t1,metasenv,_subst,t3,t4, attrs) = proof in
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
let proof3,gl3 =