From 83a7c4f405055ca9e9893f449cc73bf7f11468e6 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 29 May 2019 11:02:16 +0200
Subject: [PATCH] Fix README
---
README.md | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/README.md b/README.md
index fda7d3d6..949adfac 100644
--- a/README.md
+++ b/README.md
@@ -46,13 +46,13 @@ CPU cores.
* The subfolder [model](theories/lifetime/model) proves the core rules, which
are then sealed behind a module signature in
[lifetime.v](theories/lifetime/lifetime.v).
-* The folder [logic](theories/logic) proves the surface-level rules of [GPFSL].
- These rules are the combined version of [GPFSL]'s raw rules with the lifetime
- logic or the view-dependent invariants.
+* The folder [logic](theories/logic) proves the surface-level rules of [GPFSL]
+ *atomic-borrows-based* protocols. These rules combine [GPFSL]'s raw rules with
+ the lifetime logic rules for atomic borrows.
* The folder [typing](theories/typing) defines the domain of semantic types,
interpretations of all the judgments, as well as proofs of all typing rules.
* [type.v](theories/typing/type.v) contains the definition of a semantic type.
- * [programs.v](theories/typing/programs.v) defines the typing judgements for
+ * [programs.v](theories/typing/programs.v) defines the typing judgments for
instructions and function bodies.
* [soundness.v](theories/typing/soundness.v) contains the main soundness
theorem of the type system.
--
GitLab