diff --git a/src/spec/spec/properties.v b/src/spec/spec/properties.v
index 63cdaa0..b54c615 100644
--- a/src/spec/spec/properties.v
+++ b/src/spec/spec/properties.v
@@ -4,7 +4,7 @@
 From Coq Require Import ZArith.ZArith.
 (*Require Import common.tuplehelp common.nathelp.*)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg.
-From mathcomp Require Import ring.
+From mathcomp.algebra_tactics Require Import ring.
 Require Import ssrextra.nat ssrextra.tuple.
 Require Import spec.spec.