Remove some unused values and types

1 files changed, 0 insertions, 24 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 64f4c6dc5..29dcddbb0 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -612,30 +612,6 @@ let adjust_app_array_size f1 l1 f2 l2 =
     let extras,restl1 = Array.chop (len1-len2) l1 in
     (mkApp (f1,extras), restl1, f2, l2)
 
-(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
-   subterms of [c]; it carries an extra data [l] (typically a name
-   list) which is processed by [g na] (which typically cons [na] to
-   [l]) at each binder traversal (with name [na]); it is not recursive
-   and the order with which subterms are processed is not specified *)
-
-let map_constr_with_named_binders g f l c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
-  | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
-  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
-  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
-  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
-  | Proj (p,c) -> mkProj (p, f l c)
-  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
-  | Fix (ln,(lna,tl,bl)) ->
-      let l' = Array.fold_left (fun l na -> g na l) l lna in
-      mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-  | CoFix(ln,(lna,tl,bl)) ->
-      let l' = Array.fold_left (fun l na -> g na l) l lna in
-      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-
 (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
    immediate subterms of [c]; it carries an extra data [n] (typically
    a lift index) which is processed by [g] (which typically add 1 to