modules Evar_refiner et Typing_ev

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 0 deletions

diff --git a/kernel/generic.ml b/kernel/generic.ml
index 3e33dca7b7..6b38b72ff6 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -301,6 +301,24 @@ let occur_oper s =
   in 
   occur_rec 
 
+let process_opers_of_term p f l constr = 
+  let rec filtrec acc = function
+    | DOP0 oper        -> if p oper then ((f oper)::acc) else acc
+    | VAR _            -> acc
+    | DOP1(oper,c)     -> let newacc = filtrec acc c in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DOP2(oper,c1,c2) -> let newacc = filtrec (filtrec acc c1) c2 in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DOPN(oper,cl)    -> let newacc = (Array.fold_left filtrec acc cl) in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DOPL(oper,cl)    -> let newacc = (List.fold_left filtrec acc cl) in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DLAM(_,c)        -> filtrec acc c
+    | DLAMV(_,v)       -> Array.fold_left filtrec acc v
+    | _                -> acc
+  in 
+  filtrec l constr
+
 (* Returns the list of global variables in a term *)
 
 let global_varsl l constr =