Merge PR #9087: Add CI job building stdlib with `async-proofs on`

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