diff options
| author | Maxime Dénès | 2018-11-27 09:01:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 12:30:30 +0100 |
| commit | a984c960e63b6b1a0774cbbba63ea398100c0c3d (patch) | |
| tree | 0d591ce6a7ec69495a2a73bcd2026d013d86fec2 /theories/Strings/BinaryString.v | |
| parent | 27332ea5e0e461d1ccc6f0f7a6c329d18b45e2b9 (diff) | |
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.
Diffstat (limited to 'theories/Strings/BinaryString.v')
| -rw-r--r-- | theories/Strings/BinaryString.v | 2 |
1 files changed, 1 insertions, 1 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 |