Source file wp__.ml

(* generated by dune *)

(** @canonical Wp.AssignsCompleteness *)
module AssignsCompleteness = Wp__AssignsCompleteness

(** @canonical Wp.Auto *)
module Auto = Wp__Auto

(** @canonical Wp.Cache *)
module Cache = Wp__Cache

(** @canonical Wp.CfgAnnot *)
module CfgAnnot = Wp__CfgAnnot

(** @canonical Wp.CfgCalculus *)
module CfgCalculus = Wp__CfgCalculus

(** @canonical Wp.CfgCompiler *)
module CfgCompiler = Wp__CfgCompiler

(** @canonical Wp.CfgDump *)
module CfgDump = Wp__CfgDump

(** @canonical Wp.CfgGenerator *)
module CfgGenerator = Wp__CfgGenerator

(** @canonical Wp.CfgInfos *)
module CfgInfos = Wp__CfgInfos

(** @canonical Wp.CfgInit *)
module CfgInit = Wp__CfgInit

(** @canonical Wp.CfgWP *)
module CfgWP = Wp__CfgWP

(** @canonical Wp.Cfloat *)
module Cfloat = Wp__Cfloat

(** @canonical Wp.Cint *)
module Cint = Wp__Cint

(** @canonical Wp.Clabels *)
module Clabels = Wp__Clabels

(** @canonical Wp.Cleaning *)
module Cleaning = Wp__Cleaning

(** @canonical Wp.Cmath *)
module Cmath = Wp__Cmath

(** @canonical Wp.CodeSemantics *)
module CodeSemantics = Wp__CodeSemantics

(** @canonical Wp.Conditions *)
module Conditions = Wp__Conditions

(** @canonical Wp.Context *)
module Context = Wp__Context

(** @canonical Wp.Cstring *)
module Cstring = Wp__Cstring

(** @canonical Wp.Ctypes *)
module Ctypes = Wp__Ctypes

(** @canonical Wp.Cvalues *)
module Cvalues = Wp__Cvalues

(** @canonical Wp.Definitions *)
module Definitions = Wp__Definitions

(** @canonical Wp.Driver *)
module Driver = Wp__Driver

(** @canonical Wp.Factory *)
module Factory = Wp__Factory

(** @canonical Wp.Filter_axioms *)
module Filter_axioms = Wp__Filter_axioms

(** @canonical Wp.Filtering *)
module Filtering = Wp__Filtering

(** @canonical Wp.Footprint *)
module Footprint = Wp__Footprint

(** @canonical Wp.Generator *)
module Generator = Wp__Generator

(** @canonical Wp.Lang *)
module Lang = Wp__Lang

(** @canonical Wp.Layout *)
module Layout = Wp__Layout

(** @canonical Wp.Letify *)
module Letify = Wp__Letify

(** @canonical Wp.LogicAssigns *)
module LogicAssigns = Wp__LogicAssigns

(** @canonical Wp.LogicBuiltins *)
module LogicBuiltins = Wp__LogicBuiltins

(** @canonical Wp.LogicCompiler *)
module LogicCompiler = Wp__LogicCompiler

(** @canonical Wp.LogicSemantics *)
module LogicSemantics = Wp__LogicSemantics

(** @canonical Wp.LogicUsage *)
module LogicUsage = Wp__LogicUsage

(** @canonical Wp.Matrix *)
module Matrix = Wp__Matrix

(** @canonical Wp.Mcfg *)
module Mcfg = Wp__Mcfg

(** @canonical Wp.MemDebug *)
module MemDebug = Wp__MemDebug

(** @canonical Wp.MemEmpty *)
module MemEmpty = Wp__MemEmpty

(** @canonical Wp.MemLoader *)
module MemLoader = Wp__MemLoader

(** @canonical Wp.MemMemory *)
module MemMemory = Wp__MemMemory

(** @canonical Wp.MemRegion *)
module MemRegion = Wp__MemRegion

(** @canonical Wp.MemTyped *)
module MemTyped = Wp__MemTyped

(** @canonical Wp.MemVal *)
module MemVal = Wp__MemVal

(** @canonical Wp.MemVar *)
module MemVar = Wp__MemVar

(** @canonical Wp.MemZeroAlias *)
module MemZeroAlias = Wp__MemZeroAlias

(** @canonical Wp.MemoryContext *)
module MemoryContext = Wp__MemoryContext

(** @canonical Wp.Mstate *)
module Mstate = Wp__Mstate

(** @canonical Wp.NormAtLabels *)
module NormAtLabels = Wp__NormAtLabels

(** @canonical Wp.Passive *)
module Passive = Wp__Passive

(** @canonical Wp.Pattern *)
module Pattern = Wp__Pattern

(** @canonical Wp.Pcfg *)
module Pcfg = Wp__Pcfg

(** @canonical Wp.Pcond *)
module Pcond = Wp__Pcond

(** @canonical Wp.Plang *)
module Plang = Wp__Plang

(** @canonical Wp.ProofEngine *)
module ProofEngine = Wp__ProofEngine

(** @canonical Wp.ProofScript *)
module ProofScript = Wp__ProofScript

(** @canonical Wp.ProofSession *)
module ProofSession = Wp__ProofSession

(** @canonical Wp.ProofStrategy *)
module ProofStrategy = Wp__ProofStrategy

(** @canonical Wp.Prover *)
module Prover = Wp__Prover

(** @canonical Wp.ProverScript *)
module ProverScript = Wp__ProverScript

(** @canonical Wp.ProverSearch *)
module ProverSearch = Wp__ProverSearch

(** @canonical Wp.ProverTask *)
module ProverTask = Wp__ProverTask

(** @canonical Wp.ProverWhy3 *)
module ProverWhy3 = Wp__ProverWhy3

(** @canonical Wp.Ptip *)
module Ptip = Wp__Ptip

(** @canonical Wp.RefUsage *)
module RefUsage = Wp__RefUsage

(** @canonical Wp.Region *)
module Region = Wp__Region

(** @canonical Wp.RegionAccess *)
module RegionAccess = Wp__RegionAccess

(** @canonical Wp.RegionAnalysis *)
module RegionAnalysis = Wp__RegionAnalysis

(** @canonical Wp.RegionAnnot *)
module RegionAnnot = Wp__RegionAnnot

(** @canonical Wp.RegionDump *)
module RegionDump = Wp__RegionDump

(** @canonical Wp.Register *)
module Register = Wp__Register

(** @canonical Wp.Repr *)
module Repr = Wp__Repr

(** @canonical Wp.Rformat *)
module Rformat = Wp__Rformat

(** @canonical Wp.Script *)
module Script = Wp__Script

(** @canonical Wp.Sigma *)
module Sigma = Wp__Sigma

(** @canonical Wp.Sigs *)
module Sigs = Wp__Sigs

(** @canonical Wp.Splitter *)
module Splitter = Wp__Splitter

(** @canonical Wp.Stats *)
module Stats = Wp__Stats

(** @canonical Wp.StmtSemantics *)
module StmtSemantics = Wp__StmtSemantics

(** @canonical Wp.Strategy *)
module Strategy = Wp__Strategy

(** @canonical Wp.TacArray *)
module TacArray = Wp__TacArray

(** @canonical Wp.TacBitrange *)
module TacBitrange = Wp__TacBitrange

(** @canonical Wp.TacBittest *)
module TacBittest = Wp__TacBittest

(** @canonical Wp.TacBitwised *)
module TacBitwised = Wp__TacBitwised

(** @canonical Wp.TacChoice *)
module TacChoice = Wp__TacChoice

(** @canonical Wp.TacClear *)
module TacClear = Wp__TacClear

(** @canonical Wp.TacCompound *)
module TacCompound = Wp__TacCompound

(** @canonical Wp.TacCompute *)
module TacCompute = Wp__TacCompute

(** @canonical Wp.TacCongruence *)
module TacCongruence = Wp__TacCongruence

(** @canonical Wp.TacCut *)
module TacCut = Wp__TacCut

(** @canonical Wp.TacFilter *)
module TacFilter = Wp__TacFilter

(** @canonical Wp.TacHavoc *)
module TacHavoc = Wp__TacHavoc

(** @canonical Wp.TacInduction *)
module TacInduction = Wp__TacInduction

(** @canonical Wp.TacInstance *)
module TacInstance = Wp__TacInstance

(** @canonical Wp.TacLemma *)
module TacLemma = Wp__TacLemma

(** @canonical Wp.TacModMask *)
module TacModMask = Wp__TacModMask

(** @canonical Wp.TacNormalForm *)
module TacNormalForm = Wp__TacNormalForm

(** @canonical Wp.TacOverflow *)
module TacOverflow = Wp__TacOverflow

(** @canonical Wp.TacRange *)
module TacRange = Wp__TacRange

(** @canonical Wp.TacRewrite *)
module TacRewrite = Wp__TacRewrite

(** @canonical Wp.TacSequence *)
module TacSequence = Wp__TacSequence

(** @canonical Wp.TacShift *)
module TacShift = Wp__TacShift

(** @canonical Wp.TacSplit *)
module TacSplit = Wp__TacSplit

(** @canonical Wp.TacUnfold *)
module TacUnfold = Wp__TacUnfold

(** @canonical Wp.Tactical *)
module Tactical = Wp__Tactical

(** @canonical Wp.VC *)
module VC = Wp__VC

(** @canonical Wp.VCS *)
module VCS = Wp__VCS

(** @canonical Wp.Vlist *)
module Vlist = Wp__Vlist

(** @canonical Wp.Vset *)
module Vset = Wp__Vset

(** @canonical Wp.Warning *)
module Warning = Wp__Warning

(** @canonical Wp.Why3Provers *)
module Why3Provers = Wp__Why3Provers

(** @canonical Wp.WpApi *)
module WpApi = Wp__WpApi

(** @canonical Wp.WpContext *)
module WpContext = Wp__WpContext

(** @canonical Wp.WpPropId *)
module WpPropId = Wp__WpPropId

(** @canonical Wp.WpRTE *)
module WpRTE = Wp__WpRTE

(** @canonical Wp.WpReached *)
module WpReached = Wp__WpReached

(** @canonical Wp.WpReport *)
module WpReport = Wp__WpReport

(** @canonical Wp.WpTac *)
module WpTac = Wp__WpTac

(** @canonical Wp.WpTacApi *)
module WpTacApi = Wp__WpTacApi

(** @canonical Wp.WpTarget *)
module WpTarget = Wp__WpTarget

(** @canonical Wp.WpTipApi *)
module WpTipApi = Wp__WpTipApi

(** @canonical Wp.Wp_error *)
module Wp_error = Wp__Wp_error

(** @canonical Wp.Wp_eva *)
module Wp_eva = Wp__Wp_eva

(** @canonical Wp.Wp_parameters *)
module Wp_parameters = Wp__Wp_parameters

(** @canonical Wp.Wpo *)
module Wpo = Wp__Wpo

module Wp__ = struct end
[@@deprecated "this module is shadowed"]