Closed thery closed 8 years ago
The current opam package does not seem to handle coq 8.5:
% opam install coq-ssr-multinomials Your request can't be satisfied:
No solution found, exiting
Here is my setting:
% opam info coq-ssr-multinomials package: coq-ssr-multinomials version: dev repository: extra-dev upstream-url: https://github.com/math-comp/multinomials.git upstream-kind: git homepage: https://github.com/strub/multinomials-ssr bug-reports: https://github.com/strub/multinomials-ssr/issues author: Pierre-Yves Strub license: CeCILL-B depends: coq (>= 8.4pl4 & < 8.5~) & coq-mathcomp-ssreflect (>= 1.6 & < 1.7) & coq-mathcomp-algebra (>= 1.6 & < 1.7) installed-version: available-version: dev description: A Multinomial Library for the Mathematical Components Library.
% opam list coq
coq 8.5.0 (pinned) Formal proof management system.
% opam repo 30 [http] extra-dev https://coq.inria.fr/opam/extra-dev 20 [http] coq-core-dev https://coq.inria.fr/opam/core-dev 10 [http] coq-released https://coq.inria.fr/opam/released 0 [http] default https://opam.ocaml.org
Indeed. I have to check that it is compiling with Coq 8.5 first.
Is there some magic to have Coq files compatible with the From ... required by 8.5 to find ssreflect, while still compiling in 8.4?
From ...
👍
The current opam package does not seem to handle coq 8.5:
% opam install coq-ssr-multinomials Your request can't be satisfied:
No solution found, exiting
Here is my setting:
% opam info coq-ssr-multinomials package: coq-ssr-multinomials version: dev repository: extra-dev upstream-url: https://github.com/math-comp/multinomials.git upstream-kind: git homepage: https://github.com/strub/multinomials-ssr bug-reports: https://github.com/strub/multinomials-ssr/issues author: Pierre-Yves Strub license: CeCILL-B depends: coq (>= 8.4pl4 & < 8.5~) & coq-mathcomp-ssreflect (>= 1.6 & < 1.7) & coq-mathcomp-algebra (>= 1.6 & < 1.7) installed-version: available-version: dev description: A Multinomial Library for the Mathematical Components Library.
% opam list coq
Available packages for coq8.5:
coq 8.5.0 (pinned) Formal proof management system.
% opam repo 30 [http] extra-dev https://coq.inria.fr/opam/extra-dev 20 [http] coq-core-dev https://coq.inria.fr/opam/core-dev 10 [http] coq-released https://coq.inria.fr/opam/released 0 [http] default https://opam.ocaml.org