From 506bd1803e2d2d8249d2791b26e12ee57073d5a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Sep 2020 15:29:31 +0200
Subject: [PATCH] Add `cl_logic` folder to README.

---
 README.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/README.md b/README.md
index 07c92d7dc..f28d925e8 100644
--- a/README.md
+++ b/README.md
@@ -100,6 +100,9 @@ followed by `make build-dep`.
   modules; they may change or disappear without any notice.
 * The folder [si_logic](theories/si_logic) defines a "plain" step-indexed logic
   and shows that it is an instance of the BI interface.
+* The folder [cl_logic](theories/cl_logic) embeds classical logic in Coq,
+  following essentially the Gödel-Gentzen translation, and shows that it is an
+  instance of the BI interface.
 
 ## Case Studies
 
-- 
GitLab