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