From 95b4a54ec6a9aacffe8c11df1b443d36b9f6dda7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 12 May 2015 16:48:01 +0200
Subject: Extraction: fix the detection of the "polyprop" situation

 The ~polyprop argument wasn't propagated properly anymore,
 leading the extraction to try to operate on situations it cannot
 handle (yet). Cf Table.error_singleton_become_prop for more details.

 Regression test added.
---
 kernel/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca814f497c..088b99b9e0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -214,7 +214,7 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a
     (ty, cst)
 
 let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
-  type_of_inductive_gen env mip args
+  type_of_inductive_gen ~polyprop env mip args
 
 (* The max of an array of universes *)
 
-- 
cgit v1.2.3


From f480f07c232b4bcc4ea67bf0577e267d0fdc35f4 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 12 May 2015 17:22:09 +0200
Subject: Fix my previous commit on ~polyprop

 Oups, sorry, I should have compiled the stdlib in full. Not only
 the ~polyprop wasn't propagated properly, but Matthieu made it be
 false by default somewhere instead of true. Argl...
---
 kernel/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 088b99b9e0..4c1614bac1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -213,7 +213,7 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
-let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
+let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
   type_of_inductive_gen ~polyprop env mip args
 
 (* The max of an array of universes *)
-- 
cgit v1.2.3


From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 09:53:36 +0200
Subject: Disable precompilation for native_compute by default.

Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.

Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.

If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.

Failure to precompile is a hard error, since it is now explicitly required
by the user.
---
 kernel/nativeconv.ml  | 5 ++---
 kernel/safe_typing.ml | 4 ++--
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 75a3fc4582..1f8bfc984f 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -121,9 +121,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   aux 0
 
 let native_conv pb sigma env t1 t2 =
-  if !Flags.no_native_compiler then begin
-    let msg = "Native compiler is disabled, "^
-    "falling back to VM conversion test." in
+  if Coq_config.no_native_compiler then begin
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
     Pp.msg_warning (Pp.str msg);
     vm_conv pb env t1 t2
   end
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;
-- 
cgit v1.2.3