Adapt to split_stdlib

proux01 · Jul 22, 2024 · 1d55d08 · 1d55d08
1 parent 9ba18c4
commit 1d55d08
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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.