diff options
| author | Gaëtan Gilbert | 2019-01-08 15:57:27 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-30 12:49:28 +0100 |
| commit | f6613489304a30846af28334c040c7d4f9e4addc (patch) | |
| tree | 1b5e600288190926ee4be95ba40a1d071060e7c6 /kernel/context.mli | |
| parent | a9b141469fe3036355be95d8cf5f0bf5c240fe37 (diff) | |
Restrict universes in records.
Fix #8076.
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index 2b0d36cb8c..8acae73680 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -78,6 +78,9 @@ sig (** Map all terms in a given declaration. *) val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt + (** Map all terms, with an heterogeneous function. *) + val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt + (** Perform a given action on all terms in a given declaration. *) val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit |