search

math-comp / mczify

Micromega tactics for Mathematical Components
23 stars 8 forks source link

Package broken or opam bounds incorrect with mathcomp/mathcomp:1.17.0-coq-dev #49

Closed JasonGross closed 1 year ago

JasonGross commented 1 year ago

With opam install coq-mathcomp-zify on mathcomp/mathcomp:1.17.0-coq-dev, I see

  + (script @ line 9) $ opam install -y -v coq-record-update coq-flocq coq-mathcomp-zify
  The following actions will be performed:
    - install coq-mathcomp-zify dev
    - install coq-record-update 0.3.2
    - install coq-flocq         dev
  ===== 3 to install =====
[...]
   - File "./theories/zify_ssreflect.v", line 136, characters 30-40:
  Error: - Error: The reference Order.diff was not found in the current environment.
pi8027 commented 1 year ago

This should now be fixed by coq/opam#2688, but feel free to reopen if it is not fixed.