Phase_local_mutation (hax-engine.Hax_engine.Phase_local

module Make
  (F : 
    Features.T
      with type mutable_reference = Features.Off.mutable_reference
       and type mutable_pointer = Features.Off.mutable_pointer
       and type raw_pointer = Features.Off.raw_pointer
       and type arbitrary_lhs = Features.Off.arbitrary_lhs
       and type nontrivial_lhs = Features.Off.nontrivial_lhs
       and type monadic_action = Features.Off.monadic_action
       and type monadic_binding = Features.Off.monadic_binding
       and type for_index_loop = Features.Off.for_index_loop) : 
  sig ... end