with
Failure _ -> assert false)
| Cic.Const (uri,exp_named_subst) as t ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant (_,Some body,_,_,_) ->
CicReduction.head_beta_reduce
| Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
| Cic.Var (uri,exp_named_subst) as t ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant _ -> raise ReferenceToConstant
| Cic.CurrentProof _ -> raise ReferenceToCurrentProof
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Constant (_,Some body,_,_,_) ->
if List.exists is_active l then
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in
match o with
C.InductiveDefinition (tl,ingredients,r,_) ->
let (_,_,arity,_) = List.nth tl i in
prerr_endline (CicPp.ppterm t2 ^ "\n");
let subst1, _, _ =
CicUnification.fo_unif metasenv ctx t1 t2
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
prerr_endline "UNIFICANO\n\n\n";
subst := subst1;