From bb875065f346e25445a5fb04f84606355be1455d Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Sat, 23 Jul 2022 13:20:42 -0300
Subject: [PATCH] Update README.md

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

diff --git a/README.md b/README.md
index 5c22617b..5c81a672 100644
--- a/README.md
+++ b/README.md
@@ -3,9 +3,8 @@ Kind2
 
 Kind2 is a pure functional, lazy, non-garbage-collected, general-purpose,
 dependently typed programming language focusing on performance and usability. It
-features a blazingly fast type-checker that runs on the
-[HVM](https://github.com/kindelia/hvm) via
-[NbE](https://en.wikipedia.org/wiki/Normalisation_by_evaluation). It can also
+features a blazingly fast type-checker based on **optimal
+[normalization-by-evaluation](https://en.wikipedia.org/wiki/Normalisation_by_evaluation)**. It can also
 compile programs to HVM and [Kindelia](https://github.com/kindelia/kindelia),
 and can be used to prove and verify mathematical theorems.