From 264afb325ec8e34009cf267d418ff0ba3ceb1da5 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 20 Oct 1999 09:53:38 +0000
Subject: modules Evar_refiner et Typing_ev

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/generic.ml   | 18 ++++++++++++++++++
 kernel/generic.mli  |  2 ++
 kernel/reduction.ml |  2 ++
 3 files changed, 22 insertions(+)

(limited to 'kernel')

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 = 
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 49ec5bfbe5..cad600a50c 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -81,6 +81,8 @@ val occur_opern : 'a -> 'a term -> bool
 val occur_oper0 : 'a -> 'a term -> bool
 val occur_var : identifier -> 'a term -> bool
 val occur_oper : 'a -> 'a term -> bool
+val process_opers_of_term : 
+  ('a -> bool) -> ('a -> 'b) -> 'b list -> 'a term -> 'b list
 val dependent : 'a term -> 'a term -> bool
 val global_varsl : identifier list -> 'a term -> identifier list
 val global_vars : 'a term -> identifier list
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ac32e2eabd..7119729c7d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1425,3 +1425,5 @@ let rec strip_all_casts t =
     | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c)
     | VAR _ as t -> t
     | Rel _ as t -> t
+
+
-- 
cgit v1.2.3