Skip to content

Commit 60eaa1f

Browse files
committed
Adapt to coq/coq#18590
1 parent 9d1cd5e commit 60eaa1f

File tree

1 file changed

+6
-3
lines changed

1 file changed

+6
-3
lines changed

coq-menhirlib/src/Alphabet.v

+6-3
Original file line numberDiff line numberDiff line change
@@ -156,10 +156,13 @@ Class Finite (A:Type) := {
156156

157157
(** An alphabet is both [ComparableLeibnizEq] and [Finite]. **)
158158
Class Alphabet (A:Type) := {
159-
AlphabetComparable :> Comparable A;
160-
AlphabetComparableLeibnizEq :> ComparableLeibnizEq AlphabetComparable;
161-
AlphabetFinite :> Finite A
159+
AlphabetComparable : Comparable A;
160+
AlphabetComparableLeibnizEq : ComparableLeibnizEq AlphabetComparable;
161+
AlphabetFinite : Finite A
162162
}.
163+
#[global] Existing Instance AlphabetComparable.
164+
#[global] Existing Instance AlphabetComparableLeibnizEq.
165+
#[global] Existing Instance AlphabetFinite.
163166

164167
(** The [Numbered] class provides a conveniant way to build [Alphabet] instances,
165168
with a good computationnal complexity. It is mainly a injection from it to

0 commit comments

Comments
 (0)