wip

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 ')'
 ;;

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;