Filter gamma out from substitution list in squareapply

types/types.ml

@@ -3537,6 +3537,15 @@ module Tallying = struct
     ) Var.Set.empty ll
 
   let is_identity = List.for_all (CS.E.is_empty)
+  let identity = [CS.E.empty]
+
+  let filter f sl =
+    if is_identity sl then sl else
+    List.fold_left (fun acc si ->
+      let e = CS.E.filter (fun v _ -> f v) si in
+      if CS.E.is_empty e then acc else e::acc
+    ) [] sl
+
 
 end
 
@@ -3587,7 +3596,8 @@ exception FoundApply of t * int * int * Tallying.CS.sl
     s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
 let apply_raw delta s t =
   Tallying.NormMemoHash.clear Tallying.memo_norm;
-  let gamma = var (Var.mk "Gamma") in
+  let vgamma = Var.mk "Gamma" in
+  let gamma = var vgamma in
   let cgamma = cons gamma in
   (* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
   let ai = ref [| |]
@@ -3625,7 +3635,11 @@ let apply_raw delta s t =
       done;
       tallying i i;
       loop (i+1)
-    with FoundApply (res, i, j, sl) -> sl, get ai i, get aj j, res
+    with FoundApply (res, i, j, sl) ->
+      (* we remove gamma from the substitution list as it is only used
+         here by the algorithm *)
+      let sl = (Tallying.filter (fun v -> not(Var.equal v vgamma)) sl) in
+      (sl, get ai i, get aj j, res)
   in
   loop 0
 

types/types.mli

@@ -451,6 +451,8 @@ module Tallying : sig
   val domain : CS.sl -> Var.Set.t
   val codomain : CS.sl -> Var.Set.t
   val is_identity : CS.sl -> bool
+  val identity : CS.sl
+  val filter : (Var.t -> bool) -> CS.sl -> CS.sl
 
 end