aboutsummaryrefslogtreecommitdiffstats
path: root/MenhirLib/Alphabet.v
diff options
context:
space:
mode:
Diffstat (limited to 'MenhirLib/Alphabet.v')
-rw-r--r--MenhirLib/Alphabet.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v
index 29070e3d..530e3b4a 100644
--- a/MenhirLib/Alphabet.v
+++ b/MenhirLib/Alphabet.v
@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
-From Coq Require Import Omega List Syntax Relations RelationClasses.
+From Coq Require Import Omega List Relations RelationClasses.
+Import ListNotations.
Local Obligation Tactic := intros.