From fb9e31fddf5a71310e247407095c911bfd911e43 Mon Sep 17 00:00:00 2001
From: Jonathan Chan <jonathanhwchan@gmail.com>
Date: Fri, 18 Apr 2025 16:52:02 -0400
Subject: [PATCH] Minor edits

---
 cbpv.mng | 4 ++--
 cbpv.pdf | 4 ++--
 cbpv.tex | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/cbpv.mng b/cbpv.mng
index 399482c..4b93e1e 100644
--- a/cbpv.mng
+++ b/cbpv.mng
@@ -8,7 +8,7 @@
 \usepackage[margin=1in]{geometry}
 \usepackage{enumitem,float,booktabs,xspace,doi}
 \usepackage{amsmath,amsthm,amssymb}
-\usepackage[capitalize,nameinlink]{cleveref}
+\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
 \usepackage{mathpartir,mathtools,stmaryrd}
 
 \setlist{nosep}
@@ -436,7 +436,7 @@ so I present them here as admissible rules.
 All the hard work happens in these lemmas;
 the fundamental theorem of soundness of syntactic typing with respect to semantic typing
 then follows directly.
-Normalization holds as an easy corollary.
+Normalization holds as a corollary.
 
 {\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$[[G ⊧ v : A]]$}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
diff --git a/cbpv.pdf b/cbpv.pdf
index 16b0dcc..17b26c8 100644
--- a/cbpv.pdf
+++ b/cbpv.pdf
@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:78c4c356efb79eec148c56f072fe085288f4b09595c706789818f1bd09439a42
-size 262187
+oid sha256:5ac9dfc36f6dc1a73d3878b7c4408b89a4e7b44653d9f6f759289da3c0919b46
+size 262118
diff --git a/cbpv.tex b/cbpv.tex
index 76fa25b..9c95ee3 100644
--- a/cbpv.tex
+++ b/cbpv.tex
@@ -8,7 +8,7 @@
 \usepackage[margin=1in]{geometry}
 \usepackage{enumitem,float,booktabs,xspace,doi}
 \usepackage{amsmath,amsthm,amssymb}
-\usepackage[capitalize,nameinlink]{cleveref}
+\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
 \usepackage{mathpartir,mathtools,stmaryrd}
 
 \setlist{nosep}
@@ -436,7 +436,7 @@ so I present them here as admissible rules.
 All the hard work happens in these lemmas;
 the fundamental theorem of soundness of syntactic typing with respect to semantic typing
 then follows directly.
-Normalization holds as an easy corollary.
+Normalization holds as a corollary.
 
 {\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}