aboutsummaryrefslogtreecommitdiffstats
path: root/MenhirLib/Interpreter_complete.v
diff options
context:
space:
mode:
Diffstat (limited to 'MenhirLib/Interpreter_complete.v')
-rw-r--r--MenhirLib/Interpreter_complete.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/MenhirLib/Interpreter_complete.v b/MenhirLib/Interpreter_complete.v
index ec69592b..51f2524b 100644
--- a/MenhirLib/Interpreter_complete.v
+++ b/MenhirLib/Interpreter_complete.v
@@ -11,7 +11,8 @@
(* *)
(****************************************************************************)
-From Coq Require Import List Syntax Arith.
+From Coq Require Import List Arith.
+Import ListNotations.
From Coq.ssr Require Import ssreflect.
Require Import Alphabet Grammar.
Require Automaton Interpreter Validator_complete.