| C.Var (u,exp_named_subst) ->
if List.mem u !don then [] else
(don := u::!don;
- aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph))
+ aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))
| C.MutInd (u,_,exp_named_subst) ->
if List.mem u !don || eq u uri then
[]
else
begin
don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
with
- | C.InductiveDefinition (l,_,_) ->
+ | C.InductiveDefinition (l,_,_,_) ->
List.fold_left (
fun y (_,_,t,l') ->
y @ (aux t) @
else
begin
don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
- | C.InductiveDefinition (l,_,_) ->
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
+ | C.InductiveDefinition (l,_,_,_) ->
List.fold_left (
fun x (_,_,_t,l') ->
x @ aux t @
List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
and aux_obj ?(boo=false) (t,_) =
(match t with
- C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
+ C.Constant (_,Some te,ty,v,_) -> aux te @ aux ty @
List.fold_left (
fun l u ->
l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)))
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.Constant (_,None,ty,v) -> aux ty @
+ | C.Constant (_,None,ty,v,_) -> aux ty @
List.fold_left (
fun l u ->
l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)))
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
+ | C.CurrentProof (_,conjs,te,ty,v,_) -> aux te @ aux ty @
List.fold_left (
fun l u ->
l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)))
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
+ | C.Variable (_,Some bo,ty,v,_) -> aux bo @ aux ty @
List.fold_left (
fun l u ->
l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)))
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.Variable (_,None ,ty,v) -> aux ty @
+ | C.Variable (_,None ,ty,v,_) -> aux ty @
List.fold_left (
fun l u ->
l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)))
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v
- | C.InductiveDefinition (l,v,_) ->
+ | C.InductiveDefinition (l,v,_,_) ->
(List.fold_left (
fun x (_,_,t,l') ->
x @ aux t @ List.fold_left (
(List.fold_left
(fun l u ->
l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph)))
+ (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
[] v)
)
in