From ce0924599497800773ebc95b392e678926ea1820 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 08:49:45 +0100
Subject: User flags for coqtop/coqc in Makefile and CI build template

---
 Makefile.build | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index ec9b81dba4..0a73562467 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -44,6 +44,9 @@ NO_RECALC_DEPS ?=
 # Non-empty runs the checker on all produced .vo files:
 VALIDATE ?=
 
+# When non-empty, passed as extra arguments to coqtop/coqc:
+COQUSERFLAGS ?=
+
 # Output file names for timed builds
 TIME_OF_BUILD_FILE               ?= time-of-build.log
 TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
@@ -191,7 +194,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 # the output format of the unix command time. For instance:
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR)
+COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
 BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
 LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
-- 
cgit v1.2.3


From 27332ea5e0e461d1ccc6f0f7a6c329d18b45e2b9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 08:57:45 +0100
Subject: Add CI job building stdlib with `-async-proofs on`

---
 .gitlab-ci.yml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 65a8a0cb88..b1a805b59e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -225,6 +225,13 @@ build:egde:dune:dev:
     OPAM_SWITCH: edge
     DUNE_TARGET: world
 
+build:base+async:
+  <<: *build-template
+  stage: test
+  variables:
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
+    COQUSERFLAGS: "-async-proofs on"
+
 windows64:
   <<: *windows-template
   variables:
-- 
cgit v1.2.3


From a984c960e63b6b1a0774cbbba63ea398100c0c3d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 09:01:43 +0100
Subject: Avoid Fixpoint without struct nor body in stdlib

As reported in #9060, the STM does not handle such constructions
properly. They are anyway fragile, for example Guarded reports a failure
if run at the end of the scripts, so this patch is an improvement.
---
 theories/Strings/BinaryString.v | 2 +-
 theories/Strings/HexString.v    | 2 +-
 theories/Strings/OctalString.v  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Strings/BinaryString.v b/theories/Strings/BinaryString.v
index 6df0a9170a..a2bb1763f5 100644
--- a/theories/Strings/BinaryString.v
+++ b/theories/Strings/BinaryString.v
@@ -48,7 +48,7 @@ Module Raw.
               end
        end.
 
-  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p}
     : to_N (of_pos p rest) base
       = to_N rest match base with
                   | N0 => N.pos p
diff --git a/theories/Strings/HexString.v b/theories/Strings/HexString.v
index 9ea93c909e..9fa8e0ccf2 100644
--- a/theories/Strings/HexString.v
+++ b/theories/Strings/HexString.v
@@ -120,7 +120,7 @@ Module Raw.
               end
        end.
 
-  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p}
     : to_N (of_pos p rest) base
       = to_N rest match base with
                   | N0 => N.pos p
diff --git a/theories/Strings/OctalString.v b/theories/Strings/OctalString.v
index fe8cc9aae9..78e98e451b 100644
--- a/theories/Strings/OctalString.v
+++ b/theories/Strings/OctalString.v
@@ -78,7 +78,7 @@ Module Raw.
               end
        end.
 
-  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+  Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p}
     : to_N (of_pos p rest) base
       = to_N rest match base with
                   | N0 => N.pos p
-- 
cgit v1.2.3