Update Tutorial_Chaining_Tactics.v

coq · Nov 2, 2024 · 0d3ab6e · 0d3ab6e
1 parent e967e25
commit 0d3ab6e
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/Tutorial_Chaining_Tactics.v b/src/Tutorial_Chaining_Tactics.v
@@ -38,9 +38,7 @@
 
 *)
 
-  Require Import Lia.
-
-  Section Chaining.
+Section Chaining.
   Context (A B C D E F : Type).
 
   Set Printing Parentheses.
@@ -539,4 +537,4 @@ Goal A -> B -> C -> D -> E -> F.
   Fail do 8 intros ?.
 Abort.
 
-End Chaining.
+End Chaining.