diff options
Diffstat (limited to 'kernel/vm.mli')
| -rw-r--r-- | kernel/vm.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli index bc1978663..43a42eb9c 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -64,7 +64,6 @@ external val_of_annot_switch : annot_switch -> values = "%identity" val whd_val : values -> whd val uni_lvl_val : values -> Univ.universe_level -val instantiate_universe : Univ.universe -> stack -> Univ.universe (** Arguments *) |