diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 25 |
1 files changed, 1 insertions, 24 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 86a93e935d..5d1dca14c9 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -20,6 +20,7 @@ open Libobject open Lib open Nametab open Pp +open Termops open Topconstr (*s Flags governing the computation of implicit arguments *) @@ -164,30 +165,6 @@ let is_flexible_reference env bound depth f = | Ind _ | Construct _ -> false | _ -> true -(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate - subterms of [c]; it carries an extra data [acc] which is processed by [g] at - each binder traversal; it is not recursive and the order with which - subterms are processed is not specified *) - -let iter_constr_with_full_binders g f l c = match kind_of_term 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 (na,None,t) l) c - | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c - | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c - | App (c,args) -> f l c; Array.iter (f l) args - | 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 (fun l na t -> g (na,None,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 (fun l na t -> g (na,None,t) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl - let push_lift d (e,n) = (push_rel d e,n+1) (* Precondition: rels in env are for inductive types only *) |