diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 7b5ed05bda..93a91af1d7 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -978,6 +978,15 @@ struct end +type 'a univ_abstracted = { + univ_abstracted_value : 'a; + univ_abstracted_binder : AUContext.t; +} + +let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} = + let univ_abstracted_value = f univ_abstracted_value in + {univ_abstracted_value;univ_abstracted_binder} + let hcons_abstract_universe_context = AUContext.hcons (** Universe info for cumulative inductive types: A context of |