From 70ee147275d787383e8fc0d4f7d26f0289eddd69 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Sep 2014 23:19:18 +0200
Subject: [PATCH] Use the ascii decider from the stdlib which is extracted
 correctly.

---
 theories/stringmap.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/stringmap.v b/theories/stringmap.v
index 6f542b7f..d53d2601 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.
 
-- 
GitLab