diff options
| author | Hugo Herbelin | 2018-04-06 09:55:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-12 22:23:57 +0200 |
| commit | a623c11adac7c34aae92dbeb0c5b7ecc863ce6fd (patch) | |
| tree | 9e3e46d5bdc7f34085ba7edc64ace9c4ce62d368 /kernel/constr.mli | |
| parent | 235cb6e6c243863b7270d273ceeef681eb350247 (diff) | |
Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.
This is to move a standard combinator to the place it belongs to. An
alternative could have been to put it in termops.ml, but termops.ml is
now about econstr, so, even if it makes the kernel "bigger", constr.ml
seems to be the best place for this combinator. After all, this
combinator is canonical.
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 3c9cc96a0d..d97afffc53 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -465,6 +465,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 *) |