Skip to content

Commit

Permalink
More qualified import of zify.ssrZ
Browse files Browse the repository at this point in the history
Without a qualified import `coq-mathcomp-apery` is incompatible with `coq-mathcomp-word`. See also jasmin-lang/coqword#15
  • Loading branch information
LasseBlaauwbroek authored Jan 27, 2023
1 parent 4239449 commit 1396736
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/rat_of_Z.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Require Import ZArith.
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Export ssrZ.
From mathcomp.zify Require Export ssrZ.
Require Import tactics.

Set Implicit Arguments.
Expand Down

0 comments on commit 1396736

Please sign in to comment.