Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d762a246e6..d6bd754783 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -772,9 +772,9 @@ let export ?except senv dir =
     }
   in
   let ast, values =
-    if !Flags.no_native_compiler then [], [||]
-    else
+    if !Flags.native_compiler then
       Nativelibrary.dump_library mp dir senv.env str
+    else [], [||]
   in
   let lib = {
     comp_name = dir;