aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.mli
blob: 407edea442b0c8eb681e5fc82b00c3302d820b7c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
open Names
open Cbytecodes
open Cemitcodes 
open Term
open Declarations
open Environ



val compile : env -> constr -> bytecodes * bytecodes * fv
                              (* init, fun, fv *)

val compile_constant_body : 
    env -> constant -> constr_substituted option -> bool -> bool -> body_code
                                              (* opaque *) (* boxed *)