diff options
| author | coqbot-app[bot] | 2021-03-11 11:57:46 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-11 11:57:46 +0000 |
| commit | d33266649d285b7d8ba5a7093319faa6132d6bc9 (patch) | |
| tree | a49c779eeddeb56909d3dd85f8423fde133a88fb /kernel/vmbytegen.mli | |
| parent | a40631f9fbcd0ef8c1a716010be48e3f650e8955 (diff) | |
| parent | b31c4fa57eac8162ad6b6e03f75b13afd9b76db7 (diff) | |
Merge PR #13854: Normalize evars during bytecode compilation.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
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 -> |