diff options
| author | coqbot-app[bot] | 2020-12-03 13:59:36 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-03 13:59:36 +0000 |
| commit | afbc39d8c4f24e2e8ccda0fcb861fb947f3f4c71 (patch) | |
| tree | a8be7066f13772bc04d54e92c3f9f408f1693249 /kernel/constr.mli | |
| parent | a88568e751d63d8db93450213272c8b28928dbf2 (diff) | |
| parent | 056245e24411c3f410d3e91897ad8ce97bc59587 (diff) | |
Merge PR #13548: Move *_with_full_binders variants out of the kernel.
Reviewed-by: SkySkimmer
Ack-by: herbelin
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 62f2555a7e..ed63ac507c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -478,25 +478,6 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr -(** [map_under_context_with_full_binders g f n l c] is similar to - [map_under_context_with_binders] except that [g] takes also a full - binder as argument and that only the number of binders (and not - their signature) is required *) - -val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr - -(** [map_branches_with_full_binders g f l br] is equivalent to - [map_branches_with_binders] but using - [map_under_context_with_full_binders] *) - -val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array - -(** [map_return_predicate_with_full_binders g f l p] is equivalent to - [map_return_predicate_with_binders] but using - [map_under_context_with_full_binders] *) - -val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr - (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] @@ -505,10 +486,6 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a -val fold_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b - val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a (** [map f c] maps [f] on the immediate subterms of [c]; it is |