Make (hax-engine.Hax_engine.Phase_local

Parameters

module 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

Signature

include sig ... end

module FA = F

module FB : sig ... end

module A : sig ... end

module B : sig ... end

module ImplemT : sig ... end

include ImplemT.T

val metadata : Hax_engine__Phase_utils.Metadata.t

val ditems : A.item Prelude.list -> B.item Prelude.list