From fe7f1496d2b2d8c8b3caed4110b651df11a5b683 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 11:28:12 +0200
Subject: [PATCH 1/5] fix config

---
 config | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/config b/config
index 2ad035d..32fdb66 100755
--- a/config
+++ b/config
@@ -170,9 +170,9 @@ then
     echo create deps.mk ...
     rm -f deps.mk
     touch deps.mk
-    set $base_rocqfiles
-    if test $# -gt 0
+    if test -n "$base_rocqfiles"
     then
+        set $base_rocqfiles
         echo -n ${1}o >> deps.mk
         shift
         for f in $*

From 60193239306cc1bed0cce60208af374c45886bf9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 26 Jun 2026 11:56:09 +0200
Subject: [PATCH 2/5] wip

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 83f4e0d..0a59d28 100644
--- a/Makefile
+++ b/Makefile
@@ -406,7 +406,7 @@ clean-lean: rm-lean
 
 .PHONY: rm-lean
 rm-lean:
-	if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -name $(ROOT_PATH)/%) -delete; fi
+	if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -wholename $(ROOT_PATH)/%) -delete; fi
 
 $(ROOT_PATH).lean:
 ifneq ($(SET_STI_FILES),1)

From 3730294fdc2e71eb465b20dd1fc455b3958aaed7 Mon Sep 17 00:00:00 2001
From: Ivan Martinez Comas <imcnavi20@gmail.com>
Date: Fri, 26 Jun 2026 13:07:37 +0200
Subject: [PATCH 3/5] fix make clean-lean

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 0a59d28..ce5d765 100644
--- a/Makefile
+++ b/Makefile
@@ -406,7 +406,7 @@ clean-lean: rm-lean
 
 .PHONY: rm-lean
 rm-lean:
-	if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -wholename $(ROOT_PATH)/%) -delete; fi
+	@if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -name %) -delete; fi
 
 $(ROOT_PATH).lean:
 ifneq ($(SET_STI_FILES),1)

From ac5e2b7339bf045c33542985c615a1c36aea4291 Mon Sep 17 00:00:00 2001
From: Ivan Martinez Comas <imcnavi20@gmail.com>
Date: Fri, 26 Jun 2026 15:26:31 +0200
Subject: [PATCH 4/5] explicit type of type variables

---
 xlp.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/xlp.ml b/xlp.ml
index 540b380..d11159f 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -119,8 +119,10 @@ let typ = abbrev_typ;;
 let decl_type_abbrevs oc =
   let abbrev s (k,n) =
     string oc "symbol type"; digest oc k;
-    for i=0 to n-1 do string oc " a"; int oc i done;
-    (* We can use [raw_typ] here since [b] is canonical. *)
+    if n > 0 then begin
+      string oc " (a0"; for i=1 to n-1 do string oc " a"; int oc i done;
+      string oc " : Set)"
+    end;
     string oc " ≔ "; string oc s; string oc ";\n"
   in
   MapStr.iter abbrev !map_typ_abbrev

From 7974bebdeb7692c497aba838738ec2142ba1a873 Mon Sep 17 00:00:00 2001
From: Ivan Martinez Comas <imcnavi20@gmail.com>
Date: Mon, 29 Jun 2026 17:48:17 +0200
Subject: [PATCH 5/5] indent

---
 xlp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/xlp.ml b/xlp.ml
index d986ed5..0be7b64 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -378,10 +378,10 @@ let decl_term_abbrev oc t (k,ntvs,bs) =
   string oc "symbol "; string oc n;
   if ntvs > 0 then
     begin
-    raw_update_tvs_map n ntvs; 
-    string oc " (a0";
-    for i=1 to ntvs-1 do string oc " a"; int oc i done;
-    string oc " : Set)"
+      raw_update_tvs_map n ntvs; 
+      string oc " (a0";
+      for i=1 to ntvs-1 do string oc " a"; int oc i done;
+      string oc " : Set)"
     end;
   let decl_var i b =
     string oc " (x"; int oc i; string oc ": El "; abbrev_typ oc b; char oc ')'