diff options
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 *) |