feat(engine/phases): use phase Drop_metasized in all backends

Author: W95Psp

engine/backends/coq/coq/coq_backend.ml

@@ -1085,6 +1085,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.And_mut_defsite
   |> Phases.Reconstruct_asserts

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -554,6 +554,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.Unsafe(Features.Rust)
+    |> Phases.Drop_metasized
     |> Phases.Reject.RawOrMutPointer
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_asserts

engine/backends/fstar/fstar_backend.ml

@@ -1910,6 +1910,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait

engine/backends/proverif/proverif_backend.ml

@@ -885,6 +885,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.Transform_hax_lib_inline
   |> Phases.Simplify_question_marks