From b8871d9c2df0f30b87f761441aad486297738db5 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Thu, 5 Dec 2024 10:30:53 +0100
Subject: [PATCH] Remove the implementation without FStarBinder of erased_impl.

---
 engine/backends/fstar/fstar_backend.ml | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 29c45bfa4..5c0cb4e2c 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -881,18 +881,6 @@ struct
     in
     let erased_impl name ty attrs binders =
       let name' = F.id_prime name in
-      (* let arguments =
-           match F.AST.(ty.tm) with
-           | F.AST.Product (binders, _) -> binders
-           | _ -> []
-         in
-         let generics_names =
-           arguments
-           |> List.filter_map ~f:(fun arg ->
-                  match F.AST.(arg.aqual, arg.b) with
-                  | Some ((Implicit | TypeClassArg) as arg), F.AST.Annotated (name, _) -> Some (name, arg)
-                  | _ -> None)
-         in *)
       let pat = F.AST.PatVar (name, None, []) in
       let term = F.term @@ F.AST.Var (F.lid_of_id @@ name') in
       let pat, term =