From b4f322106d129bf629d7318248c020eea5026af8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sun, 15 Dec 2024 23:06:42 +0100
Subject: [PATCH] wip

---
 xdk.ml | 18 +++++-------------
 xlp.ml |  2 +-
 2 files changed, 6 insertions(+), 14 deletions(-)

diff --git a/xdk.ml b/xdk.ml
index e12e8a3..d7d73ff 100644
--- a/xdk.ml
+++ b/xdk.ml
@@ -372,17 +372,9 @@ let subproof tvs rmap ty_su tm_su ts1 i2 oc p2 =
   (* tvbs2 is the type variables of bs2 *)
   let tvbs2 = tyvarsl bs2 in
   (* we remove from tvbs2 the variables of tvs *)
-  let tvbs2 =
-    List.fold_left
-      (fun tvbs2 tv -> if List.mem tv tvs then tvbs2 else tv::tvbs2)
-      [] tvbs2
-  in
+  let tvbs2 = remove_elts tvs tvbs2 in
   (* we extend ty_su by mapping every type variable of tvbs2 to bool *)
-  let ty_su =
-    List.fold_left
-      (fun su tv -> (bool_ty,tv)::su)
-      ty_su tvbs2
-  in
+  let ty_su = Xlp.extend_to_bool ty_su tvbs2 in
   match ty_su with
   | [] ->
      string oc "(lem"; int oc i2; list_prefix " " typ oc tvs2;
@@ -393,9 +385,9 @@ let subproof tvs rmap ty_su tm_su ts1 i2 oc p2 =
      let vs2 = List.map (inst ty_su) vs2 in
      (* ts2 is now the application of ty_su on ts2 *)
      let ts2 = List.map (inst ty_su) ts2 in
-     (* bs is the list of types obtained by applying ty_su on tvs2 *)
-     let bs = List.map (type_subst ty_su) tvs2 in
-     string oc "(lem"; int oc i2; list_prefix " " typ oc bs;
+     (* bs2 is the list of types obtained by applying ty_su on tvs2 *)
+     let bs2 = List.map (type_subst ty_su) tvs2 in
+     string oc "(lem"; int oc i2; list_prefix " " typ oc bs2;
      list_prefix " " term oc vs2; list_prefix " " (hyp_var ts1) oc ts2;
      char oc ')'
 ;;
diff --git a/xlp.ml b/xlp.ml
index 39bb356..29291af 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -445,7 +445,7 @@ let subproof tvs rmap ty_su tm_su ts1 i2 oc p2 =
      let vs2 = List.map (inst ty_su) vs2 in
      (* ts2 is now the application of ty_su on ts2 *)
      let ts2 = List.map (inst ty_su) ts2 in
-     (* bs is the list of types obtained by applying ty_su on tvs2 *)
+     (* bs2 is the list of types obtained by applying ty_su on tvs2 *)
      let bs2 = List.map (type_subst ty_su) tvs2 in
      string oc "(@lem"; int oc i2; list_prefix " " typ oc bs2;
      list_prefix " " term oc vs2; list_prefix " " (hyp_var ts1) oc ts2;