New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Workaround for #87 #90

Merged

pi8027 merged 1 commit into master from fix-sub-deprecation

Oct 14, 2023

Member

pi8027 commented Oct 14, 2023

Closes #87


          Workaround for #87

2a14b95

pi8027 commented

View reviewed changes

theories/ring.v

-                    Ring.Rnorm R_of_Z zero add opp sub one mul exp
+                (* FIXME: workaround for #87 *)
+                (forall R_of_Z zero opp add sub_ one mul exp,
+                    Ring.Rnorm R_of_Z zero add opp sub_ one mul exp

Member Author

pi8027 Oct 14, 2023

This is not an instance of the minimization shown in #87, but this change suppresses the warning anyway. (We may have to investigate it later.)

pi8027 merged commit d83ef0f into master

7 checks passed

pi8027 deleted the fix-sub-deprecation branch

October 14, 2023 13:05

pi8027 mentioned this pull request

Open

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment