From 139673650d774f0ac9edbe691715a191feebb22a Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Fri, 27 Jan 2023 06:49:22 +0100 Subject: [PATCH] More qualified import of `zify.ssrZ` Without a qualified import `coq-mathcomp-apery` is incompatible with `coq-mathcomp-word`. See also https://github.com/jasmin-lang/coqword/issues/15 --- theories/rat_of_Z.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/rat_of_Z.v b/theories/rat_of_Z.v index 2e9f553..48b4fb4 100644 --- a/theories/rat_of_Z.v +++ b/theories/rat_of_Z.v @@ -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.