From e2f1be274afa823e05c12878f9111bcfe60e3b50 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Nov 2018 23:15:03 +0100
Subject: Termops.iter_constr_with_full_binders =
 EConstr.iter_with_full_binders

---
 interp/impargs.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3