diff options
| author | Gaëtan Gilbert | 2018-10-31 13:20:41 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-31 13:36:13 +0100 |
| commit | f7472bf04801ebbda372d0c16267f9d9668ec5fa (patch) | |
| tree | 8fa224d857b362956892a8a4a759e0a3bde1cbe0 /test-suite | |
| parent | ec73ad521123e11ad8e1c6c916de48ae30b12639 (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Inductive.v | 2 |
1 files changed, 0 insertions, 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. |