How can I import mathcomp without getting the Compiled library mathcomp.ssreflect.all_ssreflect (in file /lib/mathcomp/ssreflect/all_ssreflect.vo) makes inconsistent assumptions over library Coq.Init.Notations
error?
I've the mathcomp package installed in /node_modules but it seems to override some Coq Notations.
My code is basically the same of npm-template but importing all_ssreflect from mathcomp (which is already added init_pkgs and all_pkgs wacoq options).
The notation overrides are standard, but ssreflect should load nevertheless. Are you using 0.15.0? Make sure both jscoq
and @jscoq/mathcomp
are the same version.
npm ls jscoq @jscoq/mathcomp
Shachar Itzhaky said:
The notation overrides are standard, but ssreflect should load nevertheless. Are you using 0.15.0? Make sure both
jscoq
and@jscoq/mathcomp
are the same version.
Yes, both are in 0.15.0.
Just checked again, and it only happens in wacoq, it isn't intended for mathcomp or packages?
Jscoq is completely fine.
oh for waCoq you need to install @wacoq/mathcomp
.
Sry, the two are not binary-compat. We may want to change that but currently I am not sure how.
Last updated: Jun 01 2023 at 12:01 UTC