aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_4151.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/bug_4151.v')
-rw-r--r--test-suite/bugs/closed/bug_4151.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_4151.v b/test-suite/bugs/closed/bug_4151.v
index 9ec8c01ac6..df3c9481a6 100644
--- a/test-suite/bugs/closed/bug_4151.v
+++ b/test-suite/bugs/closed/bug_4151.v
@@ -9,7 +9,7 @@ Qed.
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
Require Import Coq.Lists.SetoidList.
-Require Export Coq.Program.Program.
+Import ListNotations.
Global Set Implicit Arguments.
Global Set Asymmetric Patterns.