From bfed5bd8176b7e6d106a96f6d5296bc2d8510017 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 15 Jan 2025 12:25:25 +0100
Subject: [PATCH] add note in NOTES.md + fix typo in README.md

---
 NOTES.md  | 28 +++++++++++++++++++++++++++-
 README.md |  2 +-
 2 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/NOTES.md b/NOTES.md
index fd3591a..0ac0da6 100644
--- a/NOTES.md
+++ b/NOTES.md
@@ -1,11 +1,37 @@
 NOTES
 -----
 
+## 13/01/25
+
+Files raising a stack overflow:
+
+CONTINUOUS_AT_WINDING_NUMBER.v
+COVERING_SPACE_CEXP_PUNCTURED_PLANE.v
+E_APPROX_32.v
+HAS_INTEGRAL_TWIZZLE_INTERVAL.v
+HOMEOMORPHIC_MONOTONE_IMAGE_INTERVAL_part_56.v
+INESSENTIAL_NEIGHBOURHOOD_EXTENSION_LOGARITHM_part_3.v
+INESSENTIAL_NEIGHBOURHOOD_EXTENSION_LOGARITHM_part_4.v
+LOG2_APPROX_32_part_1.v
+LOG2_APPROX_32_part_2.v
+PI2_BOUNDS.v
+PI_APPROX_32_part_10.v
+PI_APPROX_32_part_11.v
+PI_APPROX_32_part_1.v
+PI_APPROX_32_part_2.v
+PI_APPROX_32_part_3.v
+PI_APPROX_32_part_4.v
+PI_APPROX_32_part_5.v
+PI_APPROX_32_part_6.v
+PI_APPROX_32_part_7.v
+PI_APPROX_32_part_8.v
+PI_APPROX_32_part_9.v
+SCHOTTKY_part_1.v
+
 ## 30/11/24
 
 adding the alignment of real numbers double the coq checking time:
 
-
 Performance on 30/11/24
 -----------------------
 
diff --git a/README.md b/README.md
index cebe571..b35e2ea 100644
--- a/README.md
+++ b/README.md
@@ -218,7 +218,7 @@ For instance, to translate the Multivariate library using the Coq type N for nat
 ```
 mkdir output
 cd output
-hol2dk config Multivariate/make_complex.ml HOLLight HOLLight_Real_With_N.mappings $(HOL2DK_DIR)/With_N.v BinNat Rbase Rdefinitions Rbasic_fun $(HOL2DK_DIR)/With_N.mk $(HOL2DK_DIR)/With_N.lp
+hol2dk config Multivariate/make_complex.ml HOLLight HOLLight_Real_With_N.mappings $HOL2DK_DIR/With_N.v BinNat Rbase Rdefinitions Rbasic_fun $HOL2DK_DIR/With_N.mk $HOL2DK_DIR/With_N.lp
 ```
 
 - you can then do in order: