From a5a851f55aeddaf6d985730cac3d660b39e67206 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 17 May 2019 12:28:47 +0200
Subject: [PATCH] Strings are inhabited

---
 theories/strings.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/strings.v b/theories/strings.v
index 7c674d38..989dfa95 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -23,6 +23,8 @@ Proof. solve_decision. Defined.
 Instance string_app_inj : Inj (=) (=) (String.append s1).
 Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
 
+Instance string_inhabited : Inhabited string := populate "".
+
 (* Reverse *)
 Fixpoint string_rev_app (s1 s2 : string) : string :=
   match s1 with
-- 
GitLab