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/

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 502, characters 9-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 483, characters 15-24: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 467, characters 15-31: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 77, characters 14-19: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Categories/Functor/Core.v", line 65, characters 0-45: Warning: Implicitly declaring Rewrite hint databases is deprecated. Please explicitly create "functor" [implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default] theories/Categories/Functor/Core.vo (real: 0.09, user: 0.03, sys: 0.05, mem: 100064 ko) theories/Categories/Category/Strict.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 89180 ko)

Could not find a terminator for warning: File "./theories/Categories/Category/Core.v", line 116, characters 0-63: Warning: Implicitly declaring Rewrite hint databases is deprecated. Please explicitly create "morphism" [implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default] theories/Categories/Category/Core.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 132500 ko) theories/Spaces/List/Core.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 109436 ko) theories/Types/Option.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 89464 ko) test/bugs/github1794.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 86252 ko) theories/Diagrams/Graph.vo (real: 0.09, user: 0.03, sys: 0.05, mem: 87792 ko) theories/Tactics/Nameless.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 89932 ko) theories/Axioms/Funext.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 86540 ko) theories/Axioms/PropResizing.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 85760 ko) theories/Basics/Classes.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 125784 ko) theories/Basics/Iff.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 102932 ko) theories/Basics/Numerals/Hexadecimal.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 121284 ko) theories/Basics/Predicate.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 134296 ko)

Could not find a terminator for warning: File "./theories/Categories/Category/Core.v", line 114, characters 0-63: Warning: Implicitly declaring Rewrite hint databases is deprecated. Please explicitly create "category" [implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Overture.v", line 405, characters 7-20: Warning: Autogenerated "rew_r" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default] theories/Basics/Overture.vo (real: 0.16, user: 0.10, sys: 0.05, mem: 194160 ko) theories/Basics/Numerals/Decimal.vo (real: 0.13, user: 0.07, sys: 0.06, mem: 112764 ko) theories/Basics/Tactics.vo (real: 0.18, user: 0.12, sys: 0.06, mem: 189824 ko)

Could not find a terminator for warning: File "./theories/Basics/Overture.v", line 402, characters 7-20: Warning: Autogenerated "rew" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default]