Package coq-interval @ 3.4.1

Synopsis

Coq tactics to simplify inequality proofs

Description

Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

Home page
http://coq-interval.gforge.inria.fr/
Location
gnu/packages/coq.scm (line: 454, column: 2)
License

Lint warnings

LinterMessageLocation
derivation

Report failure to compile a package to a derivation

failed to create i686-linux derivation: path ‘/gnu/store/imq41gd3q2767il9gq6mqh5cv44x09rf-guile-2.2.6.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create armhf-linux derivation: path ‘/gnu/store/9wn798a6w534mnn4f28lglbjmib9n392-zlib-1.2.11.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create aarch64-linux derivation: path ‘/gnu/store/0afbxr7962z9ci6kw840n088qsmyz8lr-guile-2.2.6.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create mips64el-linux derivation: path ‘/gnu/store/aiwgcl5dppar2s8l408bshywjybsy3nd-zlib-1.2.11.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create x86_64-linux derivation: path ‘/gnu/store/1dz7hwpizsbvz88j1g2s4c16ayjy36dz-coq-8.10.2.drv’ is not valid