From 0d3ab6e4df69330a7d575464e855129fd7156412 Mon Sep 17 00:00:00 2001
From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com>
Date: Sat, 2 Nov 2024 17:02:15 +0100
Subject: [PATCH] Update Tutorial_Chaining_Tactics.v

---
 src/Tutorial_Chaining_Tactics.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Tutorial_Chaining_Tactics.v b/src/Tutorial_Chaining_Tactics.v
index 7ad124f..e8e350c 100644
--- 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.
\ No newline at end of file
+End Chaining.