summaryrefslogtreecommitdiff
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/validator/Alphabet.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v
index f47f136..85a1689 100644
--- a/cparser/validator/Alphabet.v
+++ b/cparser/validator/Alphabet.v
@@ -290,10 +290,10 @@ apply all_list_forall.
Defined.
(** Definitions of [FSet]/[FMap] from [Comparable] **)
-Require Import OrderedType.
Require Import OrderedTypeAlt.
Require FSetAVL.
Require FMapAVL.
+Import OrderedType.
Module Type ComparableM.
Parameter t : Type.