From f7472bf04801ebbda372d0c16267f9d9668ec5fa Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 31 Oct 2018 13:20:41 +0100
Subject: No need to require List in test-suite/success/Inductive.v

Requires are slow in the debugger so removing this makes it nicer to debug.
---
 test-suite/success/Inductive.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index f07c0191f1..c2130995fc 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,7 +1,5 @@
 (* Test des definitions inductives imbriquees *)
 
-Require Import List.
-
 Inductive X : Set :=
     cons1 : list X -> X.
 
-- 
cgit v1.2.3