From 5ddd21470497648e6fdab884b65a7c606bdf0613 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 31 Jan 2020 08:40:18 +0100
Subject: [PATCH] readme

---
 README.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index df8b4a6..6582caf 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,9 @@
 # PVS proofs
 
-Encodings of PVS and manual translations of PVS prelude. Use with `lambdapi`.
+Encodings of PVS and manual translations of PVS prelude and others.
+Use with `lambdapi`.
 
-## TODO
-- simplify PVS cert encoding:
-  - no `Rule` since PTS is functional,
-  - no `Type Prop Type` rule since it does not concern products but only
-    predicate subtyping.
+## Structure
+- `prelude` contains parts of the PVS prelude
+- `adlib` contains additional libraries not in the prelude
+- `sandbox` contains miscellaneous experiments
-- 
GitLab