(install
(section (site (easycrypt theories)))
(files
(algebra/Bigalg.ec as algebra/Bigalg.ec )
(algebra/Binomial.ec as algebra/Binomial.ec )
(algebra/Group.ec as algebra/Group.ec )
(algebra/Ideal.ec as algebra/Ideal.ec )
(algebra/IntDiv.ec as algebra/IntDiv.ec )
(algebra/Number.ec as algebra/Number.ec )
(algebra/Perms.ec as algebra/Perms.ec )
(algebra/Poly.ec as algebra/Poly.ec )
(algebra/Ring.ec as algebra/Ring.ec )
(algebra/StdBigop.ec as algebra/StdBigop.ec )
(algebra/StdOrder.ec as algebra/StdOrder.ec )
(algebra/StdRing.ec as algebra/StdRing.ec )
(algebra/ZModP.ec as algebra/ZModP.ec )
(analysis/RealExp.ec as analysis/RealExp.ec )
(analysis/RealFLub.ec as analysis/RealFLub.ec )
(analysis/RealFun.ec as analysis/RealFun.ec )
(analysis/RealLub.ec as analysis/RealLub.ec )
(analysis/RealSeq.ec as analysis/RealSeq.ec )
(analysis/RealSeries.ec as analysis/RealSeries.ec )
(core/AllCore.ec as core/AllCore.ec )
(core/Bool.ec as core/Bool.ec )
(core/Core.ec as core/Core.ec )
(core/CoreInt.ec as core/CoreInt.ec )
(core/CoreMap.ec as core/CoreMap.ec )
(core/CoreReal.ec as core/CoreReal.ec )
(crypto/AdvAbsVal.ec as crypto/AdvAbsVal.ec )
(crypto/Birthday.ec as crypto/Birthday.ec )
(crypto/Commitment.ec as crypto/Commitment.ec )
(crypto/DLog.ec as crypto/DLog.ec )
(crypto/DiffieHellman.ec as crypto/DiffieHellman.ec )
(crypto/LorR.ec as crypto/LorR.ec )
(crypto/MAC.ec as crypto/MAC.ec )
(crypto/OW.ec as crypto/OW.ec )
(crypto/PKE.ec as crypto/PKE.ec )
(crypto/PKS.ec as crypto/PKS.ec )
(crypto/PROM.ec as crypto/PROM.ec )
(crypto/SecureChannels.ec as crypto/SecureChannels.ec )
(crypto/SigmaProtocol.ec as crypto/SigmaProtocol.ec )
(crypto/SplitRO.ec as crypto/SplitRO.ec )
(crypto/SymmetricEncryption.ec as crypto/SymmetricEncryption.ec )
(crypto/assumptions/AEAD.ec as crypto/assumptions/AEAD.ec )
(crypto/assumptions/CRHash.ec as crypto/assumptions/CRHash.ec )
(crypto/assumptions/DHIES.ec as crypto/assumptions/DHIES.ec )
(crypto/assumptions/MRPKE.ec as crypto/assumptions/MRPKE.ec )
(crypto/assumptions/ODH.ec as crypto/assumptions/ODH.ec )
(crypto/assumptions/PKSMK.ec as crypto/assumptions/PKSMK.ec )
(datatypes/Array.ec as datatypes/Array.ec )
(datatypes/BitEncoding.ec as datatypes/BitEncoding.ec )
(datatypes/FSet.ec as datatypes/FSet.ec )
(datatypes/FloorCeil.ec as datatypes/FloorCeil.ec )
(datatypes/Int.ec as datatypes/Int.ec )
(datatypes/IntMin.ec as datatypes/IntMin.ec )
(datatypes/List.ec as datatypes/List.ec )
(datatypes/Real.ec as datatypes/Real.ec )
(distributions/DBool.ec as distributions/DBool.ec )
(distributions/DInterval.ec as distributions/DInterval.ec )
(distributions/DJoin.ec as distributions/DJoin.ec )
(distributions/DList.ec as distributions/DList.ec )
(distributions/DMap.ec as distributions/DMap.ec )
(distributions/DProd.ec as distributions/DProd.ec )
(distributions/Dexcepted.ec as distributions/Dexcepted.ec )
(distributions/Dfilter.ec as distributions/Dfilter.ec )
(distributions/Distr.ec as distributions/Distr.ec )
(distributions/Mu_mem.ec as distributions/Mu_mem.ec )
(distributions/SDist.ec as distributions/SDist.ec )
(encryption/DDH_hybrid.ec as encryption/DDH_hybrid.ec )
(encryption/Hybrid.ec as encryption/Hybrid.ec )
(encryption/Indist.ec as encryption/Indist.ec )
(encryption/Means.ec as encryption/Means.ec )
(encryption/PKE_hybrid.ec as encryption/PKE_hybrid.ec )
(encryption/SampleBool.ec as encryption/SampleBool.ec )
(modules/EventPartitioning.ec as modules/EventPartitioning.ec )
(newth/SmtMap.ec as newth/SmtMap.ec )
(oldlibs/CyclicGroup.ec as oldlibs/CyclicGroup.ec )
(oldlibs/Cyclic_group_prime.ec as oldlibs/Cyclic_group_prime.ec )
(oldlibs/OldDistr.ec as oldlibs/OldDistr.ec )
(oldlibs/OldFMap.ec as oldlibs/OldFMap.ec )
(oldlibs/PrimeField.ec as oldlibs/PrimeField.ec )
(oldlibs/Prime_field.ec as oldlibs/Prime_field.ec )
(prelude/Logic.ec as prelude/Logic.ec )
(prelude/Pervasive.ec as prelude/Pervasive.ec )
(prelude/Tactics.ec as prelude/Tactics.ec )
(query_counting/OracleBounds.ec as query_counting/OracleBounds.ec )
(structure/Discrete.ec as structure/Discrete.ec )
(structure/FinType.ec as structure/FinType.ec )
(structure/Finite.ec as structure/Finite.ec )
(structure/Quotient.ec as structure/Quotient.ec )
(tactics/AlgTactic.ec as tactics/AlgTactic.ec )
(tactics/FelTactic.ec as tactics/FelTactic.ec )
(algebra/Bigop.eca as algebra/Bigop.eca )
(algebra/Matrix.eca as algebra/Matrix.eca )
(algebra/Monoid.eca as algebra/Monoid.eca )
(crypto/pke/PKE_CPA.eca as crypto/pke/PKE_CPA.eca )
(crypto/PRF.eca as crypto/PRF.eca )
(crypto/PRG.eca as crypto/PRG.eca )
(crypto/PRP.eca as crypto/PRP.eca )
(crypto/prp_prf/Strong_RP_RF.eca as crypto/prp_prf/Strong_RP_RF.eca )
(crypto/RndExcept.eca as crypto/RndExcept.eca )
(crypto/ROM.eca as crypto/ROM.eca )
(crypto/ske/CCA1.eca as crypto/ske/CCA1.eca )
(crypto/ske/CCA.eca as crypto/ske/CCA.eca )
(crypto/ske/CPA.eca as crypto/ske/CPA.eca )
(crypto/ske/NewSKE.eca as crypto/ske/NewSKE.eca )
(datatypes/BitWord.eca as datatypes/BitWord.eca )
(datatypes/Tuple.eca as datatypes/Tuple.eca )
(datatypes/Word.eca as datatypes/Word.eca )
(looping/FoldProc.eca as looping/FoldProc.eca )
(looping/IterProc.eca as looping/IterProc.eca )
(modules/PlugAndPray.eca as modules/PlugAndPray.eca )
(modules/Pr_half.eca as modules/Pr_half.eca )
(modules/RndProd.eca as modules/RndProd.eca )
(query_counting/Counter.eca as query_counting/Counter.eca )
(structure/Subtype.eca as structure/Subtype.eca )
)
)