Deplacement de iter_constr_with_full_binders dans Termops

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

3 files changed, 29 insertions, 24 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 86a93e935d..5d1dca14c9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
 open Lib
 open Nametab
 open Pp
+open Termops
 open Topconstr
 
 (*s Flags governing the computation of implicit arguments *)
@@ -164,30 +165,6 @@ let is_flexible_reference env bound depth f =
     | Ind _ | Construct _ -> false
     |  _ -> true
 
-(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
-   subterms of [c]; it carries an extra data [acc] which is processed by [g] at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
-
-let iter_constr_with_full_binders g f l c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
-  | Cast (c,t) -> f l c; f l t
-  | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
-  | App (c,args) -> f l c; Array.iter (f l) args
-  | Evar (_,args) -> Array.iter (f l) args
-  | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
-  | Fix (_,(lna,tl,bl)) -> 
-      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
-      Array.iter (f l) tl;
-      Array.iter (f l') bl
-  | CoFix (_,(lna,tl,bl)) ->
-      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
-      Array.iter (f l) tl;
-      Array.iter (f l') bl
-
 let push_lift d (e,n) = (push_rel d e,n+1)
 
 (* Precondition: rels in env are for inductive types only *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a36be94fcd..23f9a7ffc7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -314,6 +314,30 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
       let fd = array_map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd
 
+(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
+   subterms of [c]; it carries an extra data [acc] which is processed by [g] at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+let iter_constr_with_full_binders g f l c = match kind_of_term c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,t) -> f l c; f l t
+  | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
+  | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
+  | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+  | App (c,args) -> f l c; Array.iter (f l) args
+  | Evar (_,args) -> Array.iter (f l) args
+  | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
+  | Fix (_,(lna,tl,bl)) -> 
+      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      Array.iter (f l) tl;
+      Array.iter (f l') bl
+  | CoFix (_,(lna,tl,bl)) ->
+      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      Array.iter (f l) tl;
+      Array.iter (f l') bl
+
 (***************************)
 (* occurs check functions  *)                         
 (***************************)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index ca5e5139df..af75cfd2d1 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -67,6 +67,10 @@ val map_constr_with_full_binders :
 val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
+val iter_constr_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> 
+    constr -> unit
+
 (**********************************************************************)
 
 val strip_head_cast : constr -> constr