diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 0f13bb18..4cbe795a 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -102,7 +102,7 @@ jobs:
           export HOLLIGHT_DIR=`pwd`/hol-light
           mkdir -p output/hol_upto_arith
           cd output/hol_upto_arith
-          hol2dk link hol_upto_arith
+          hol2dk config hol_upto_arith.ml HOLLight
           make split
           make -j3 lp
           make -j3 v
diff --git a/CHANGES.md b/CHANGES.md
index be1d8382..160083c5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,11 +3,24 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
-## Unrelease
+## Unreleased
 
 ### Added
 
 - alignment of the type of reals and basic functions on reals
+- command nbp
+- renamings to handle Multivariate
+
+### Changed
+
+- command link renamed into config and improved
+- update to work with HOL-Light 3.0
+- minimize dependencies in spec files
+- theory_hol.lp: rename T into ⊤ and F into ⊥
+
+### Fixed
+
+- handling of type variables occurring in a proof but not in a statement
 
 ## 2.0.0 (2024-04-23)
 
diff --git a/Makefile b/Makefile
index 450a05ad..5a835000 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,8 @@
 BASE := $(shell if test -f BASE; then cat BASE; fi)
 ROOT_PATH := $(shell if test -f ROOT_PATH; then cat ROOT_PATH; else echo HOLLight; fi)
 ERASING := $(shell if test -f ERASING; then cat ERASING; fi)
-REQUIRING := $(shell if test -f REQUIRING; then cat REQUIRING; else echo $(ROOT_PATH); fi)
+REQUIRING := $(shell if test -f REQUIRING; then cat REQUIRING; fi)
+VOFILES := $(shell if test -f VOFILES; then cat VOFILES; fi)
 
 MAX_PROOF = 500_000
 MAX_ABBREV = 2_000_000
@@ -137,6 +138,7 @@ lp-abbrevs: $(MIN_FILES:%.min=%.lp)
 
 .PHONY: clean-lp
 clean-lp: rm-lp rm-lpo-mk rm-mk rm-min rm-max rm-idx rm-brv rm-brp rm-typ rm-sed rm-lpo rm-siz clean-lpo clean-v
+	rm -f lpo.mk
 
 .PHONY: rm-lp
 rm-lp:
@@ -222,6 +224,7 @@ endif
 
 .PHONY: clean-v
 clean-v: rm-v clean-vo
+	rm -f vo.mk
 
 .PHONY: rm-v
 rm-v:
@@ -231,7 +234,8 @@ ifeq ($(INCLUDE_VO_MK),1)
 include vo.mk
 
 vo.mk: lpo.mk
-	sed -e 's/\.lp/.v/g' -e "s/: theory_hol.vo/: $(ROOT_PATH).vo theory_hol.vo/" -e "s/theory_hol.vo:/theory_hol.vo: $(ROOT_PATH).vo/" lpo.mk > $@
+	cp deps.mk $@
+	sed -e 's/\.lp/.v/g' -e "s/^theory_hol.vo:/theory_hol.vo: $(VOFILES) /" lpo.mk >> $@
 endif
 
 .PHONY: dep
diff --git a/README.md b/README.md
index 20ecd5b9..6e7c75f8 100644
--- a/README.md
+++ b/README.md
@@ -200,28 +200,32 @@ Translating HOL-Light proofs to Lambdapi and Coq
 - [coq-hol-light-real](https://github.com/Deducteam/coq-hol-light-real)
 - [coq-fourcolor-reals](https://github.com/coq-community/fourcolor/blob/master/coq-fourcolor-reals.opam)
 
-For not cluttering HOL-Light sources with the many generated files, we suggest to proceed as follows. For instance, for generating the proofs of the `Logic` library, do:
+**Procedure after dumping:**
+
+- create a directory where all files will be generated:
+```
+mkdir output
+```
+
+- setup the directory with all the required files:
 ```
-cd $HOLLIGHT_DIR/Logic
-hol2dk dump-simp make.ml
-mkdir -p ~/output-hol2dk/Logic
-cd ~/output-hol2dk/Logic
-hol2dk link Logic/make.ml HOLLight_Real.HOLLight_Real --root-path $HOL2DK_DIR/HOLLight.v Rdefinitions Rbasic_fun Raxioms
+cd output
+hol2dk config $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk]
 ```
-This will create files and add links to files needed to generate, translate and check proofs.
+Do `hol2dk config` to get more details.
 
-You can then do in order:
-- `make` to get the list of targets and variables
-- `make split` to generate a file for each theorem
-- `make -j$jobs lp` to translate HOL-Light proofs to Lambdapi
-- `make -j$jobs lpo` to check Lambdapi files (optional)
-- `make -j$jobs v` to translate Lambdapi files to Coq files
-- `make -j$jobs vo` to check Coq files
+- you can then do in order:
+  * `make` to get the list of targets and variables
+  * `make split` to generate a file for each theorem
+  * `make -j$jobs lp` to translate HOL-Light proofs to Lambdapi
+  * `make -j$jobs lpo` to check Lambdapi files (optional)
+  * `make -j$jobs v` to translate Lambdapi files to Coq files
+  * `make -j$jobs vo` to check Coq files
 
-To speed up lp file generation for some theorems with very big proofs, you can write in a file called `BIG_FILES` a list of theorem names (lines starting with `#` are ignored). See for instance [BIG_FILES](https://github.com/Deducteam/hol2dk/blob/main/BIG_FILES). You can also change the default values of the options `--max-proof-size` and `--max-abbrev-size` as follows:
+To speed up lp file generation for some theorems with very big proofs, you can write in a file named `BIG_FILES` a list of theorem names (lines starting with `#` are ignored). See for instance [BIG_FILES](https://github.com/Deducteam/hol2dk/blob/main/BIG_FILES). You can also change the default values of the options `--max-proof-size` and `--max-abbrev-size` as follows:
 - `make -j$jobs MAX_PROOF=500_000 MAX_ABBREV=2_000_000 lp`
 
-Remark: for the checking of generated Coq files to not fail because of lack of RAM, we generate for each theorem `${thm}.lp` one or several files for its proof, and a file `${thm}_spec.lp` declaring this theorem as an axiom. Moreover, each other theorem proof using `${thm}` requires `${thm}_spec` instead of `${thm}`. 
+**Remark:** for the checking of generated Coq files to not fail because of lack of RAM, we generate for each theorem `${thm}.lp` one or several files for its proof, and a file `${thm}_spec.lp` declaring this theorem as an axiom. Moreover, each other theorem proof using `${thm}` requires `${thm}_spec` instead of `${thm}`.
 
 Performances
 ------------
@@ -236,7 +240,7 @@ On a machine with 32 processors i9-13950HX, 64 Gb RAM, Hol2dk master, HOL-Light
 Translating HOL-Light proofs to Dedukti
 ---------------------------------------
 
-Requirement: dedukti 2.7
+**Requirement:** dedukti 2.7
 
 The Makefile commands above are not implemented for Dedukti yet. It is however possible to translate HOL-Light proofs to Dedukti in parallel by using the following older and less efficient commands:
 
diff --git a/add-links b/add-links
deleted file mode 100755
index 010ecc4f..00000000
--- a/add-links
+++ /dev/null
@@ -1,141 +0,0 @@
-#!/bin/sh
-
-if test -z "$HOL2DK_DIR"
-then
-    echo "HOL2DK_DIR is not set"
-    exit 1
-fi
-
-if test -z "$HOLLIGHT_DIR"
-then
-    echo "HOLLIGHT_DIR is not set"
-    exit 1
-fi
-
-usage() {
-    cat <<__EOF__
-usage: `basename $0` hollight_file.ml [coq_mod] ... [--root-path coq_file.v] [--erasing erasing.lp] [coq_mod] ...
-
-arguments:
-  hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR
-  coq_file.v: coq file imported in all generated coq files (mandatory if coq modules are given)
-  erasing.lp: mappings between lambdapi and coq
-  coq_mod: coq module that needs to be imported in generated files
-
-effect in the current directory:
-- create a file COMMAND containing the command used to create links
-- create a file BASE containing the base name of hollight_file.ml
-- create a file ROOT_PATH containing the base name of coq_file.v
-- create a file REQUIRING containing the coq modules and root path in the order they are given 
-- create a file lambdapi.pkg
-- create a file _CoqProject
-- create a file ERASING containing the name of erasing.lp
-- add links to coq_file.v and other files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of hollight_file
-__EOF__
-}
-
-error() {
-    echo error: $1
-    echo
-    usage
-    exit 1
-}
-
-parse_args() {
-    if test $# -ne 0; then
-        case $1 in
-            --root-path)
-                if test -z "$root_path_arg"
-                then
-                    if test $# -eq 1
-                    then
-                        error 'missing --root-path argument'
-                    else
-                        root_path_arg=$2
-                        requiring="$requiring `basename $2 .v`"
-                        shift 2
-                        parse_args $*
-                    fi
-                else
-                    error 'too many --root-path options'
-                fi;;
-            --erasing)
-                if test -z "$erasing_arg"
-                then
-                    if test $# -eq 1
-                    then
-                        error 'missing --erasing argument'
-                    else
-                        erasing_arg=$2
-                        shift 2
-                        parse_args $*
-                    fi
-                else
-                    error 'too many --erasing options'
-                fi;;
-            *)
-                if test -z "$hollight_file"
-                then
-                    hollight_file=$1
-                    shift
-                    parse_args $*
-                else
-                    requiring="$requiring $1"
-                    shift
-                    parse_args $*
-                fi;;
-        esac
-    fi
-}
-
-echo create COMMAND ...
-echo '#!/bin/sh' > COMMAND
-echo $0 $* >> COMMAND
-chmod a+x COMMAND
-
-parse_args $*
-if test -n "$requiring" -a -z "$root_path_arg"
-then
-    error "the --root-path option is mandatory when coq modules are given"
-fi
-
-base=`basename $hollight_file .ml`
-echo create BASE ...
-echo $base > BASE
-
-root_path=`basename ${root_path_arg:-HOLLight} .v`
-echo create ROOT_PATH ...
-echo $root_path > ROOT_PATH
-
-echo create lambdapi.pkg ...
-echo "package_name = $root_path" > lambdapi.pkg
-echo "root_path = $root_path" >> lambdapi.pkg
-
-echo create _CoqProject ...
-echo "-R . $root_path ." > _CoqProject
-
-echo create ERASING ...
-echo ${erasing_arg:-$HOL2DK_DIR/erasing.lp} > ERASING
-
-if test -z "$requiring"
-then
-    requiring=${root_path}.${root_path}
-fi
-echo create REQUIRING ...
-echo $requiring > REQUIRING
-
-coq_file=${root_path_arg:-$HOL2DK_DIR/HOLLight.v}
-echo ln -f -s $coq_file
-ln -f -s $coq_file
-
-for f in theory_hol.dk theory_hol.lp Makefile BIG_FILES
-do
-    echo ln -f -s $HOL2DK_DIR/$f
-    ln -f -s $HOL2DK_DIR/$f
-done
-
-for ext in prf nbp sig thm pos use
-do
-    echo ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
-    ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
-done
diff --git a/config b/config
new file mode 100755
index 00000000..fc735739
--- /dev/null
+++ b/config
@@ -0,0 +1,162 @@
+#!/bin/sh
+
+if test -z "$HOL2DK_DIR"
+then
+    echo "HOL2DK_DIR is not set"
+    exit 1
+fi
+
+if test -z "$HOLLIGHT_DIR"
+then
+    echo "HOLLIGHT_DIR is not set"
+    exit 1
+fi
+
+usage() {
+    cat <<__EOF__
+usage: `basename $0` [--erasing $erasing.lp] $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk]
+
+arguments:
+  $erasing.lp: mappings between lambdapi and coq
+  $hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR
+  $root_path: name of the generated library
+  coq_file_or_module: coq modules that needs to be imported in generated files
+  $file.mk: dependencies of vo files given in arguments
+
+effect in the current directory:
+- create a file CONFIG containing the command used to create links
+- create a file BASE containing the base name of $hollight_file.ml
+- create a file ROOT_PATH containing $root_path
+- create a file lambdapi.pkg
+- create a file _CoqProject
+- create a file ERASING containing $erasing.lp
+- create a file REQUIRING containing the list of Coq module names that need to be imported (in the same order as they are given in the command)
+- create a file VOFILES containing the list of Coq module names corresponding to the Coq files given in arguments with file extension ".vo"
+- add links to $file.mk, the Coq files given in argument and other files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of $hollight_file.ml
+__EOF__
+}
+
+error() {
+    echo error: $1
+    echo
+    usage
+    exit 1
+}
+
+parse_args() {
+    if test $# -ne 0; then
+        case $1 in
+            --erasing)
+                if test -z "$erasing"
+                then
+                    if test $# -eq 1
+                    then
+                        error 'missing --erasing argument'
+                    else
+                        erasing=$2
+                        shift 2
+                        parse_args $*
+                    fi
+                else
+                    error 'too many --erasing options'
+                fi;;
+            *.ml)
+                if test -z "$hollight_file"
+                then
+                    hollight_file=$1
+                    shift
+                    parse_args $*
+                else
+                    error 'too many ml files'
+                fi;;
+            *.mk)
+                if test -z "$mk_file"
+                then
+                    mk_file=$1
+                    shift
+                    parse_args $*
+                else
+                    error 'too many make files'
+                fi;;
+            *.v)
+                if test -z "$root_path"
+                then
+                    error 'the root_path must be given before Coq files'
+                else
+                    coq_files="$coq_files $1"
+                    vo_files="$vo_files `basename $1`o"
+                    requiring="$requiring $root_path.`basename $1 .v`"
+                    shift
+                    parse_args $*
+                fi;;
+            *)
+                if test -z "$root_path"
+                then
+                    root_path=$1
+                else
+                    requiring="$requiring $1"
+                fi
+                shift
+                parse_args $*;;
+        esac
+    fi
+}
+
+echo create CONFIG ...
+echo '#!/bin/sh' > CONFIG
+echo $0 $* >> CONFIG
+chmod a+x CONFIG
+
+parse_args $*
+if test -z "$root_path"
+then
+    error 'missing root_path'
+fi
+
+echo create BASE ...
+echo `basename $hollight_file .ml` > BASE
+
+echo create ROOT_PATH ...
+echo $root_path > ROOT_PATH
+
+echo create lambdapi.pkg ...
+echo "package_name = $root_path" > lambdapi.pkg
+echo "root_path = $root_path" >> lambdapi.pkg
+
+echo create _CoqProject ...
+echo "-R . $root_path ." > _CoqProject
+
+echo create ERASING ...
+echo ${erasing:-$HOL2DK_DIR/erasing.lp} > ERASING
+
+echo create REQUIRING ...
+echo $requiring > REQUIRING
+
+echo create VOFILES ...
+echo $vo_files > VOFILES
+
+if test -z "$mk_file"
+then
+    touch deps.mk
+else
+    echo ln -f -s $mk_file deps.mk
+    ln -f -s $mk_file deps.mk
+fi
+
+for f in $coq_files
+do
+    echo ln -f -s $f
+    ln -f -s $f
+done
+
+for f in theory_hol.dk theory_hol.lp Makefile BIG_FILES
+do
+    echo ln -f -s $HOL2DK_DIR/$f
+    ln -f -s $HOL2DK_DIR/$f
+done
+
+for ext in prf nbp sig thm pos use
+do
+    echo ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
+    ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
+done
diff --git a/dune b/dune
index 59d0f32c..5543ad11 100644
--- a/dune
+++ b/dune
@@ -5,7 +5,7 @@
 )
 
 (install
- (files HOLLight.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch add-links Makefile dep-lpo dep-vo progress README.md)
+ (files HOLLight.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch config Makefile dep-lpo dep-vo progress README.md)
  (section share)
  (package hol2dk)
 )
diff --git a/main.ml b/main.ml
index 6910b5ec..5e3513ea 100644
--- a/main.ml
+++ b/main.ml
@@ -492,7 +492,7 @@ and command = function
   | ["unpatch" as s] -> call_script s []
   | "unpatch"::_ -> wrong_nb_args()
 
-  | "link"::args -> call_script "add-links" args
+  | "config"::args -> call_script "config" args
 
   | ["dump";f] -> dump true f (basename_ml f)
   | "dump"::_ -> wrong_nb_args()
diff --git a/renaming.lp b/renaming.lp
index bf9cb2d0..d13a6f11 100644
--- a/renaming.lp
+++ b/renaming.lp
@@ -95,6 +95,10 @@ builtin "dollardollar_def" ≔ ﹩﹩_def;
 builtin "longarrow" ≔ ⭬;
 builtin "longarrow_def" ≔ ⭬_def;
 
+builtin "N'" ≔ N;
+builtin "N''" ≔ N';
+builtin "N'''" ≔ N'';
+
 builtin "R'" ≔ R;
 builtin "R''" ≔ R';