From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/cbytegen.mli | 45 +++++++++++++++------------------------------
 1 file changed, 15 insertions(+), 30 deletions(-)

(limited to 'kernel/cbytegen.mli')

diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index c0f48641..abab58b6 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -1,42 +1,27 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Cbytecodes
 open Cemitcodes
-open Term
+open Constr
 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 *)
+val compile : fail_on_error:bool ->
 	      ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
 (** init, fun, fv *)
 
-val compile_constant_body : bool ->
-			    env -> constant_universes option -> constant_def -> body_code option
+val compile_constant_body : fail_on_error:bool ->
+			    env -> constant_universes -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
-val compile_alias : Names.constant -> body_code
-
-(** spiwack: this function contains the information needed to perform
-            the static compilation of int31 (trying and obtaining
-            a 31-bit integer in processor representation at compile time) *)
-val compile_structured_int31 : bool -> constr array ->
-                               structured_constant
-
-(** this function contains the information needed to perform
-        the dynamic compilation of int31 (trying and obtaining a
-        31-bit integer in processor representation at runtime when
-        it failed at compile time *)
-val dynamic_int31_compilation : bool -> comp_env ->
-                                block array ->
-                                int -> bytecodes -> bytecodes
-
-(*spiwack: template for the compilation n-ary operation, invariant: n>=1.
-           works as follow: checks if all the arguments are non-pointers
-           if they are applies the operation (second argument) if not
-           all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
-                             constr array -> int -> bytecodes-> bytecodes
-
-(*spiwack: compiling function to insert dynamic decompilation before
-           matching integers (in case they are in processor representation) *)
-val int31_escape_before_match : bool -> bytecodes -> bytecodes
+val compile_alias : Names.Constant.t -> body_code
-- 
cgit v1.2.3