diff options
Diffstat (limited to 'kernel/vmbytegen.mli')
| -rw-r--r-- | kernel/vmbytegen.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli index aef7ac3d6b..c724cad5ec 100644 --- a/kernel/vmbytegen.mli +++ b/kernel/vmbytegen.mli @@ -15,8 +15,10 @@ open Declarations open Environ (** Should only be used for monomorphic terms *) -val compile : fail_on_error:bool -> - ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option +val compile : + fail_on_error:bool -> ?universes:int -> + env -> (existential -> constr option) -> constr -> + (bytecodes * bytecodes * fv) option (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> |