diff --git a/src/Classes.v b/src/Classes.v
index bc8741d4..1d55df69 100644
--- a/src/Classes.v
+++ b/src/Classes.v
@@ -1,4 +1,4 @@
-From Coq Require Import List Morphisms Recdef ZArith ZArith.Znat Arith.
+From Coq Require Import List Morphisms Recdef ZArith Znat Arith.
 From QuickChick  Require Import Sets Tactics Producer Generators Enumerators.
 
 Set Bullet Behavior "Strict Subproofs".
diff --git a/src/LazyList.v b/src/LazyList.v
index 3c5e7c34..26bc5c13 100644
--- a/src/LazyList.v
+++ b/src/LazyList.v
@@ -344,7 +344,7 @@ Fixpoint filter_LazyList {A} (p : A -> bool) (l : LazyList A) :=
                  else filter_LazyList p (t tt)
   end.
 
-Require Import Coq.Logic.ClassicalFacts.
+From Coq.Logic Require Import ClassicalFacts.
 
 Axiom EM : excluded_middle.
 
diff --git a/src/TacticsUtil.v.cppo b/src/TacticsUtil.v.cppo
index 584ebba3..1e0b4f8e 100644
--- a/src/TacticsUtil.v.cppo
+++ b/src/TacticsUtil.v.cppo
@@ -27,7 +27,7 @@ Ltac2 Notation "inv" h(ident) := inv_tac h.
 Local Ltac2 exfalso_tac () := ltac1:(exfalso).
 Ltac2 Notation "exfalso" := exfalso_tac ().
 
-Local Ltac2 lia_ltac1 () := ltac1:(micromega.Lia.lia).
+Local Ltac2 lia_ltac1 () := ltac1:(Lia.lia).
 Ltac2 Notation "lia" := lia_ltac1 ().
 
 Ltac2 inv := fun (h : ident) =>  inversion h; subst.