From 5ebff492a0d4ec3ddf1c3554a2b2fc71c7714c34 Mon Sep 17 00:00:00 2001
From: zhouzhezz <zorichzorich@gmail.com>
Date: Fri, 8 Mar 2024 19:53:54 -0500
Subject: [PATCH] fix

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

diff --git a/README.md b/README.md
index f870f2a..43419e6 100644
--- a/README.md
+++ b/README.md
@@ -93,7 +93,7 @@ val[@assertRty] add: (p:Path.t)⇢(path:{v:Path.t | true})→(content:{v:Bytes.t
 
 ### Coq proofs in the Docker Image
 
-The Coq proofs of our core language **λ<sup>E</sup>** are located in the `formalization/` directory. See `formalization/README.md`.
+The Coq proofs of our core language **λ<sup>E</sup>** are located in the `formalization/` directory. To build and check the Coq formalization, simply run `make` in the formalization directory. See `formalization/README.md`.
 
 ## Step-by-Step Instructions
 
@@ -393,13 +393,14 @@ EFFOP := string
 LIT :=
 | "true"
 | "false"
+| INT
 | VAR
 | OP VAR ...
 
 PROP :=
 | LIT
 | "implies" PROP PROP
-| "iff" PROP PRO
+| "iff" PROP PROP
 | PROP "&&" PROP
 | PROP "||" PROP
 | "not" PROP