Coq tactics to simplify inequality proofs
Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.
| Linter | Message | Location |
|---|---|---|
| input-labels Identify input labels that do not match package names | label 'flocq' does not match package name 'coq-flocq' | |
| input-labels Identify input labels that do not match package names | label 'bignums' does not match package name 'coq-bignums' | |
| input-labels Identify input labels that do not match package names | label 'coquelicot' does not match package name 'coq-coquelicot' | |
| input-labels Identify input labels that do not match package names | label 'mathcomp' does not match package name 'coq-mathcomp' | |
| optional-tests Make sure tests are only run when requested | the 'check' phase should respect #:tests? | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f8ed7409c60> input: ("_" "static")> | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7fa7aa068c60> input: ("_" "static")> | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f5755cb9c60> input: ("_" "static")> | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f119da52c60> input: ("_" "static")> |