Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4, actions/upload-artifact@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

Option Asymmetric Patterns No Implicits is deprecated since 9.3.

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 47, characters 0-73: Warning: Option Asymmetric Patterns No Implicits is deprecated since 9.3. [deprecated-option-since-9.3,deprecated-since-9.3,deprecated-option,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Notations.v", line 232, characters 0-97: Warning: For backwards compatibility non left recursive notations declared at level 200 are actually at level 10, with any right-recursion being at level 200. In the future level 200 will be treated as a normal level. To keep the current behaviour, use "at level 10", remove any "right associativity" annotation, and if right recursive add "x at level 200" where "x" is the last argument. [at-level-200-changed,deprecated-since-9.3,deprecated,default] theories/Basics/Notations.vo (real: 0.06, user: 0.02, sys: 0.03, mem: 74756 ko)

Could not find a terminator for warning: File "./theories/Basics/Notations.v", line 114, characters 0-104: Warning: For backwards compatibility non left recursive notations declared at level 200 are actually at level 10, with any right-recursion being at level 200. In the future level 200 will be treated as a normal level. To keep the current behaviour, use "at level 10", remove any "right associativity" annotation, and if right recursive add "x at level 200" where "x" is the last argument. [at-level-200-changed,deprecated-since-9.3,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Notations.v", line 7, characters 0-145: Warning: For backwards compatibility non left recursive notations declared at level 200 are actually at level 10, with any right-recursion being at level 200. In the future level 200 will be treated as a normal level. To keep the current behaviour, use "at level 10", remove any "right associativity" annotation, and if right recursive add "x at level 200" where "x" is the last argument. [at-level-200-changed,deprecated-since-9.3,deprecated,default]