diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 512f38cedd..8327ff1644 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -360,6 +360,14 @@ sig end +type 'a univ_abstracted = { + univ_abstracted_value : 'a; + univ_abstracted_binder : AUContext.t; +} +(** A value with bound universe levels. *) + +val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted + (** Universe info for cumulative inductive types: A context of universe levels with universe constraints, representing local universe variables and constraints, together with an array of |