- aux ty @ aux te @
- (List.fold_left (fun x t -> x @ (aux t)) [] patterns)
- | C.Fix (no, funs) ->
- List.fold_left (fun x (_,_,b,c) -> x @ (aux b) @ (aux c)) [] funs
- | C.CoFix (no,funs) ->
- 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 @
- List.fold_left (
- fun l u ->
- l @ if eq u uri then [] else
- (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 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 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 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 CicUniv.empty_ugraph u)))
- [] v
- | C.InductiveDefinition (l,v,_,_) ->
- (List.fold_left (
- fun x (_,_,t,l') ->
- x @ aux t @ List.fold_left (
- fun y (_,t) -> y @ aux t)
- [] l')
- [] l) @
- (List.fold_left
- (fun l u ->
- l @ if eq u uri then [] else
- (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
- [] v)
- )
+ aux ty; aux te; (List.iter (fun t -> aux t) patterns)
+ | C.Fix (no, funs) -> List.iter (fun (_,_,b,c) -> aux b; aux c) funs
+ | C.CoFix (no,funs) -> List.iter (fun (_,b,c) -> aux b; aux c) funs
+ | _ -> ()
+ and aux_obj = function
+ | C.Constant (_,Some te,ty,v,_)
+ | C.Variable (_,Some te,ty,v,_) ->
+ aux te;
+ aux ty;
+ List.iter
+ (fun u ->
+ if is_not_visited u then
+ (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
+ v
+ | C.Constant (_,None, ty, v,_)
+ | C.Variable (_,None, ty, v,_) ->
+ aux ty;
+ List.iter
+ (fun u ->
+ if is_not_visited u then
+ (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
+ v
+ | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
+ | C.InductiveDefinition (l,v,_,_) ->
+ List.iter
+ (fun (_,_,t,l') ->
+ aux t;
+ List.iter (fun (_,t) -> aux t) l')
+ l;
+ List.iter
+ (fun u ->
+ if is_not_visited u then
+ (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
+ v