(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            )
  )
)