diff options
| author | Maxime Dénès | 2017-12-14 17:23:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-14 17:23:13 +0100 |
| commit | 1853470c78d1a8aa2525dd57bbfce1064d359ff2 (patch) | |
| tree | d0af37b803fd6113e9fdc12f37501af3c8eba7ae /config | |
| parent | 84e570d7c532f16104157b806da714906fdf26b3 (diff) | |
| parent | 4554a860ffdcb30bf5711bd52f443484f9f950d9 (diff) | |
Merge PR #6264: [kernel] Patch allowing to disable VM reduction.
Diffstat (limited to 'config')
| -rw-r--r-- | config/coq_config.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 40661f4284..1666df0bde 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -76,4 +76,5 @@ val wwwbugtracker : string val wwwstdlib : string val localwwwrefman : string -val no_native_compiler : bool +val bytecode_compiler : bool +val native_compiler : bool |