From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 kernel/cemitcodes.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cemitcodes.mli')

diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 54b92b9121..10f3a6087a 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
-  | BCalias of constant Univ.puniverses
+  | BCalias of constant
   | BCconstant
 
 
-- 
cgit v1.2.3