diff options
| author | Gaëtan Gilbert | 2018-11-06 23:15:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:08:46 +0100 |
| commit | e2f1be274afa823e05c12878f9111bcfe60e3b50 (patch) | |
| tree | 049787bda6baf9aeaebeda9b3bc69ef339f89a33 /engine | |
| parent | fa1301c9364a3f34fa6b7d6c7e54b5a8c1db19e9 (diff) | |
Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 28 | ||||
| -rw-r--r-- | engine/termops.mli | 1 |
2 files changed, 2 insertions, 27 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]."] (**********************************************************************) |