nat: least common multiple #2207
Merged
Annotations
2 warnings
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./test/Tactics/napply.v", line 16, characters 44-57:
Warning: Tactic Notation nrapply (uconstr) is deprecated since 2025-03-11.
nrapply was renamed to napply and will be removed soon
[deprecated-tactic-notation-since-2025-03-11,deprecated-since-2025-03-11,deprecated-tactic-notation,deprecated,default]
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./test/Tactics/napply.v", line 17, characters 44-58:
Warning: Tactic Notation snrapply (uconstr) is deprecated since 2025-03-11.
snrapply was renamed to snapply and will be removed soon
[deprecated-tactic-notation-since-2025-03-11,deprecated-since-2025-03-11,deprecated-tactic-notation,deprecated,default]
test/Tactics/napply.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 133644 ko)
test/WildCat/Opposite.vo (real: 0.25, user: 0.16, sys: 0.08, mem: 360156 ko)
theories/Tactics/EquivalenceInduction.vo (real: 0.59, user: 0.50, sys: 0.09, mem: 360900 ko)
theories/Axioms/Univalence.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 104968 ko)
theories/Classes/implementations/ne_list.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 152100 ko)
theories/Functorish.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 136244 ko)
theories/Spaces/BinInt/Core.vo (real: 0.14, user: 0.08, sys: 0.06, mem: 155812 ko)
theories/Types.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 112192 ko)
theories/Cubical/PathCube.vo (real: 3.24, user: 3.13, sys: 0.10, mem: 447812 ko)
theories/Universes/TruncType.vo (real: 0.35, user: 0.25, sys: 0.10, mem: 358068 ko)
theories/Spaces/Nat/Arithmetic.vo (real: 0.23, user: 0.14, sys: 0.08, mem: 207352 ko)
theories/Colimits/Coeq.vo (real: 1.93, user: 1.81, sys: 0.11, mem: 401996 ko)
theories/WildCat/Adjoint.vo (real: 0.59, user: 0.50, sys: 0.09, mem: 369420 ko)
theories/Spaces/Nat/Division.vo (real: 0.67, user: 0.59, sys: 0.08, mem: 366096 ko)
theories/Categories/Functor/Paths.vo (real: 0.35, user: 0.26, sys: 0.09, mem: 359740 ko)
theories/Categories/NaturalTransformation/Paths.vo (real: 0.17, user: 0.10, sys: 0.07, mem: 247520 ko)
theories/Categories/InitialTerminalCategory/Core.vo (real: 0.12, user: 0.06, sys: 0.06, mem: 135092 ko)
theories/WildCat/Products.vo (real: 1.93, user: 1.81, sys: 0.11, mem: 458316 ko)
theories/Categories/Functor/Prod/Universal.vo (real: 0.19, user: 0.11, sys: 0.07, mem: 246440 ko)
theories/Categories/SetCategory/Core.vo (real: 0.12, user: 0.06, sys: 0.06, mem: 160900 ko)
theories/Categories/Functor/Composition/Laws.vo (real: 0.28, user: 0.20, sys: 0.08, mem: 357924 ko)
theories/Categories/NaturalTransformation/Dual.vo (real: 0.09, user: 0.03, sys: 0.05, mem: 111672 ko)
theories/Categories/GroupoidCategory/Dual.vo (real: 0.13, user: 0.07, sys: 0.05, mem: 185568 ko)
theories/Categories/Functor/Sum.vo (real: 0.28, user: 0.20, sys: 0.08, mem: 358836 ko)
theories/Categories/SetCategory/Functors/SetProp.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 135712 ko)
theories/Categories/SetCategory/Morphisms.vo (real: 0.20, user: 0.13, sys: 0.07, mem: 270608 ko)
theories/Categories/Profunctor/Core.vo (real: 0.10, user: 0.03, sys: 0.06, mem: 114484 ko)
theories/Categories/ExponentialLaws/Tactics.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 111000 ko)
theories/Categories/Adjoint/UnitCounit.vo (real: 0.13, user: 0.07, sys: 0.05, mem: 156076 ko)
theories/Categories/Grothendieck/ToSet/Core.vo (real: 0.14, user: 0.09, sys: 0.05, mem: 168372 ko)
theories/Categories/CategoryOfSections/Core.vo (real: 0.14, user: 0.08, sys: 0.06, mem: 163904 ko)
theories/Categories/Structure/Core.vo (real: 0.16, user: 0.09, sys: 0.07, mem: 206104 ko)
theories/Metatheory/Core.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 126368 ko)
theories/ExcludedMiddle.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 147396 ko)
theories/Spaces/Pos.vo (real: 0.09, user: 0.03, sys: 0.06, mem: 108284 ko)
test/bugs/github1382.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 133044 ko)
theories/Cubical/DPathCube.vo (real: 0.37, user: 0.28, sys: 0.08, mem: 359068 ko)
test/bugs/github726.vo (real: 0.10, user: 0.04, sys: 0.06, mem: 126492 ko)
theories/Classes/interfaces/ua_algebra.vo (real: 0.16, user: 0.10, sys: 0.06, mem: 225916 ko)
theories/Algebra/Universal/Algebra.vo (real: 0.39, user: 0.30, sys: 0.08, mem: 359312 ko)
theories/Diagrams/Diagram.vo (real: 0.23, user: 0.14, sys: 0.09, mem: 278224 ko)
theories/Colimits/CoeqUnivProp.vo (real: 0.49, user: 0.40, sys: 0.08, mem: 383156 ko)
theories/Equiv/Relational.vo (real: 0.15, user: 0.08, s
|
Loading