diff options
| author | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
| commit | a205bb9f2a93396aad154ec50f6f122cbd46811c (patch) | |
| tree | cd1ad9834fa9e6391193b377cc4533f9eba702c5 /kernel/nativecode.mli | |
| parent | 81535edc4b21015bd63d23e57ca9d707b4b71f6b (diff) | |
| parent | 131ac2af3778a741f5f33e212ef4a57f7a91d20a (diff) | |
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
Diffstat (limited to 'kernel/nativecode.mli')
| -rw-r--r-- | kernel/nativecode.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f8b..42f2cbc2e4 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -10,7 +10,7 @@ open Names open Constr open Declarations -open Pre_env +open Environ open Nativelambda (** This file defines the mllambda code generation phase of the native |