diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:25:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 15:25:42 +0100 |
| commit | 720ee2730684cc289cef588482323d177e0bea59 (patch) | |
| tree | e4deb55f090c3eb447f676a5f3529ca3b8fdd2d3 /kernel/context.mli | |
| parent | d5722a22c9ae4dec43f8c444fbebb1b1072fb686 (diff) | |
| parent | f6613489304a30846af28334c040c7d4f9e4addc (diff) | |
Merge PR #9317: Restrict universes in records.
Ack-by: SkySkimmer
Reviewed-by: mattam82
Reviewed-by: ppedrot
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 |