diff options
| author | Maxime Dénès | 2018-10-26 11:07:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-26 11:07:19 +0200 |
| commit | 4ca847d9a656a861bd11e042044a7544c420dde8 (patch) | |
| tree | 00dfc2a65d64b3f1ffcbfda5bd6b55e57c35f7e7 /kernel/constr.mli | |
| parent | 94de044826495d8b1d11b9d4b78fb7a7648813e0 (diff) | |
| parent | a623c11adac7c34aae92dbeb0c5b7ecc863ce6fd (diff) | |
Merge PR #7186: Moving `fold_constr_with_full_binders` to a place
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index c012f04260..8753c20eac 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -470,6 +470,10 @@ 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 + (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) |