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

Author: W95Psp

engine/backends/coq/coq/coq_backend.ml

@@ -1086,6 +1086,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

@@ -555,6 +555,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

@@ -1911,6 +1911,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

@@ -887,6 +887,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