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/cbytegen.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/cbytegen.mli')

diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 1128f0d0b7..c0f48641ce 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -4,17 +4,17 @@ open Term
 open Declarations
 open Pre_env
 
-
+(** Should only be used for monomorphic terms *)
 val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
-	      env -> constr -> (bytecodes * bytecodes * fv) option
+	      ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
 (** init, fun, fv *)
 
-val compile_constant_body : bool -> 
-			    env -> constant_def -> body_code option
+val compile_constant_body : bool ->
+			    env -> constant_universes option -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
-val compile_alias : pconstant -> body_code
+val compile_alias : Names.constant -> body_code
 
 (** spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
-- 
cgit v1.2.3