Skip to content

Commit

Permalink
Remove the implementation without FStarBinder of erased_impl.
Browse files Browse the repository at this point in the history
  • Loading branch information
maximebuyse committed Dec 5, 2024
1 parent cc3f619 commit b8871d9
Showing 1 changed file with 0 additions and 12 deletions.
12 changes: 0 additions & 12 deletions engine/backends/fstar/fstar_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down

0 comments on commit b8871d9

Please sign in to comment.