diff options
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]."] (**********************************************************************) |