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 /dev/base_include | |
| 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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions