| 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,_,_) ->
List.fold_left (
else
begin
don := u::!don;
- (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
- CicUniv.empty_ugraph) with
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
| C.InductiveDefinition (l,_,_) ->
List.fold_left (
fun x (_,_,_t,l') ->
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 @
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 @
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 @
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 @
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,_) ->
(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