diff --git a/theories/strings.v b/theories/strings.v index 7c674d38ab38e54839a4c5572c595e96391b1e47..5c07137409dcca3073c26c7f63fceef9259a6908 100644 --- a/theories/strings.v +++ b/theories/strings.v @@ -17,7 +17,7 @@ Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope. Arguments String.append : simpl never. (** * Decision of equality *) -Instance assci_eq_dec : EqDecision ascii := ascii_dec. +Instance ascii_eq_dec : EqDecision ascii := ascii_dec. Instance string_eq_dec : EqDecision string. Proof. solve_decision. Defined. Instance string_app_inj : Inj (=) (=) (String.append s1).