From 63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:16:57 +0100
Subject: Start fixing the tests

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

(limited to 'README.md')

diff --git a/README.md b/README.md
index 0530a0da..82ff3944 100644
--- a/README.md
+++ b/README.md
@@ -83,9 +83,9 @@ to display a detailed documentation.
 Files generated by the Lean backend import the `Base` package from Aeneas.
 To use those files in Lean, create a new Lean package using `lake new`,
 overwrite the `lean-toolchain` with the one inside `./backends/lean`,
-and add `Base` as a dependency in the `lakefile.lean`:
+and add `base` as a dependency in the `lakefile.lean`:
 ```
-require Base from "PATH_TO_AENEAS_REPO/backends/lean"
+require base from "PATH_TO_AENEAS_REPO/backends/lean"
 ```
 
 ## Targeted Subset And Current Limitations
-- 
cgit v1.2.3