From dad635d8e7ac5485935ff888c9b22acd8a1cf196 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 30 Sep 2014 16:18:44 -0400 Subject: [PATCH] Handle storage specifiers property. --- theories/pretty.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/pretty.v b/theories/pretty.v index 9cfd1f25..a8dc87ee 100644 --- a/theories/pretty.v +++ b/theories/pretty.v @@ -4,6 +4,8 @@ Require Export numbers option. Require Import Ascii String ars. Infix "+:+" := String.append (at level 60, right associativity) : C_scope. +Arguments String.append _ _ : simpl never. + 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