Use the ascii decider from the stdlib which is extracted correctly.

70ee1472 · Robbert Krebbers · 8da8fbc7 · 70ee1472
Commit 70ee1472 authored Sep 12, 2014 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 2 deletions

theories/stringmap.v theories/stringmap.v +1 -2

No files found.
--- 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.