summaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cemitcodes.mli')
-rw-r--r--kernel/cemitcodes.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index cec90130..10f3a608 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of constant Univ.puniverses
+ | Reloc_getglobal of constant
type patch = reloc_info * int
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
type body_code =
| BCdefined of to_patch
- | BCallias of constant Univ.puniverses
+ | BCalias of constant
| BCconstant