Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders

4 files changed, 7 insertions, 33 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 64048777ad..98300764df 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -767,33 +767,7 @@ let fold_constr_with_binders sigma g f n acc c =
    each binder traversal; it is not recursive and the order with which
    subterms are processed is not specified *)
 
-let iter_constr_with_full_binders sigma g f l c =
-  let open RelDecl in
-  match EConstr.kind sigma 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 (LocalAssum (na,t)) l) c
-  | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
-  | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
-  | App (c,args) -> f l c; Array.iter (f l) args
-  | Proj (p,c) -> f l c
-  | 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_i (fun i l na t ->
-        g (LocalAssum (na, EConstr.Vars.lift i 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_i (fun i l na t ->
-        g (LocalAssum (na, EConstr.Vars.lift i t)) l)
-        l lna tl
-    in
-    Array.iter (f l) tl;
-    Array.iter (f l') bl
+let iter_constr_with_full_binders = EConstr.iter_with_full_binders
 
 (***************************)
 (* occurs check functions  *)
diff --git a/engine/termops.mli b/engine/termops.mli
index 6c3d4fa612..eef8452e64 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -88,6 +88,7 @@ val iter_constr_with_full_binders : Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> unit) -> 'a ->
   constr -> unit
+[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
 
 (**********************************************************************)
 
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d8582d856e..d024a9e808 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -19,7 +19,6 @@ open Decl_kinds
 open Lib
 open Libobject
 open EConstr
-open Termops
 open Reductionops
 open Constrexpr
 open Namegen
@@ -200,16 +199,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
 	acc.(i) <- update pos rig acc.(i)
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
 	if strict then () else
-          iter_constr_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders sigma push_lift (frec false) ed c
     | Proj (p,c) when rig ->
       if strict then () else
-        iter_constr_with_full_binders sigma push_lift (frec false) ed c
+        iter_with_full_binders sigma push_lift (frec false) ed c
     | Case _ when rig ->
 	if strict then () else
-          iter_constr_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders sigma push_lift (frec false) ed c
     | Evar _ -> ()
     | _ ->
-        iter_constr_with_full_binders sigma push_lift (frec rig) ed c
+        iter_with_full_binders sigma push_lift (frec rig) ed c
   in
   let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
   acc
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 14358dd02a..10d8451947 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -759,6 +759,6 @@ let control_only_guard env sigma c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    iter_constr_with_full_binders sigma EConstr.push_rel iter env c
+    EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c
   in
   iter env c