(install
  (section (site (easycrypt theories)))
  (files
      (algebra/Bigalg.ec               as algebra/Bigalg.ec)
      (algebra/Bigop.eca               as algebra/Bigop.eca)
      (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/Matrix.eca              as algebra/Matrix.eca)
      (algebra/Monoid.eca              as algebra/Monoid.eca)
      (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.eca                 as crypto/LorR.eca)
      (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/PRF.eca                  as crypto/PRF.eca)
      (crypto/PRG.eca                  as crypto/PRG.eca)
      (crypto/PROM.ec                  as crypto/PROM.ec)
      (crypto/PRP.eca                  as crypto/PRP.eca)
      (crypto/ROM.eca                  as crypto/ROM.eca)
      (crypto/RndExcept.eca            as crypto/RndExcept.eca)
      (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)
      (crypto/pke/PKE_CPA.eca          as crypto/pke/PKE_CPA.eca)
      (crypto/prp_prf/Strong_RP_RF.eca as crypto/prp_prf/Strong_RP_RF.eca)
      (crypto/ske/CCA.eca              as crypto/ske/CCA.eca)
      (crypto/ske/CCA1.eca             as crypto/ske/CCA1.eca)
      (crypto/ske/CPA.eca              as crypto/ske/CPA.eca)
      (crypto/ske/NewSKE.eca           as crypto/ske/NewSKE.eca)
      (datatypes/Array.ec              as datatypes/Array.ec)
      (datatypes/BitEncoding.ec        as datatypes/BitEncoding.ec)
      (datatypes/BitWord.eca           as datatypes/BitWord.eca)
      (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)
      (datatypes/Tuple.eca             as datatypes/Tuple.eca)
      (datatypes/Word.eca              as datatypes/Word.eca)
      (datatypes/Xint.ec               as datatypes/Xint.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)
      (looping/FoldProc.eca            as looping/FoldProc.eca)
      (looping/IterProc.eca            as looping/IterProc.eca)
      (modules/EventPartitioning.ec    as modules/EventPartitioning.ec)
      (modules/PlugAndPray.eca         as modules/PlugAndPray.eca)
      (modules/Pr_half.eca             as modules/Pr_half.eca)
      (modules/RndProd.eca             as modules/RndProd.eca)
      (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/Counter.eca      as query_counting/Counter.eca)
      (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)
      (structure/Subtype.eca           as structure/Subtype.eca)
      (structure/WF.ec                 as structure/WF.ec)
      (tactics/AlgTactic.ec            as tactics/AlgTactic.ec)
      (tactics/CHoareTactic.ec         as tactics/CHoareTactic.ec)
      (tactics/FelTactic.ec            as tactics/FelTactic.ec)
  )
)