diff --git a/theories/stringmap.v b/theories/stringmap.v index 6f542b7f99402588d2076929f49e13c94d9042d0..d53d2601c5836202d2f1bcc011fe98df16131c13 100644 --- a/theories/stringmap.v +++ b/theories/stringmap.v @@ -7,8 +7,7 @@ and guarantees logarithmic-time operations. *) Require Export fin_maps. Require Import Ascii String list pmap mapset. -Instance assci_eq_dec (a1 a2 : ascii) : Decision (a1 = a2). -Proof. solve_decision. Defined. +Instance assci_eq_dec : ∀ a1 a2, Decision (a1 = a2) := ascii_dec. Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2). Proof. solve_decision. Defined.