Allègement du noyau

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

2 files changed, 0 insertions, 36 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 47bd656aea..bb22475230 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -479,32 +479,6 @@ let fold_constr f acc c = match kind_of_term c with
       let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
       Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
 
-(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
-   subterms of [c] starting from [acc] and proceeding from left to
-   right according to the usual representation of the constructions as
-   [fold_constr] but it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive *)
-
-let fold_constr_with_binders g f n acc c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> acc
-  | Cast (c,t) -> f n (f n acc c) t
-  | Prod (_,t,c) -> f (g n) (f n acc t) c
-  | Lambda (_,t,c) -> f (g n) (f n acc t) c
-  | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
-  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
-  | Evar (_,l) -> Array.fold_left (f n) acc l
-  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
-  | Fix (_,(lna,tl,bl)) -> 
-      let n' = iterate g (Array.length tl) n in
-      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
-  | CoFix (_,(lna,tl,bl)) ->
-      let n' = iterate g (Array.length tl) n in
-      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 f c] iters [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 1867cc4505..2c8e9be3f0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -453,16 +453,6 @@ val subst_mps : substitution -> constr -> constr
 
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
-(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
-   subterms of [c] starting from [acc] and proceeding from left to
-   right according to the usual representation of the constructions as
-   [fold_constr] but it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive *)
-
-val fold_constr_with_binders :
-  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
-
 (* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)