_CoqProject

-R src/FCF FCF
-R src/HMAC HMAC
src/FCF/Admissibility.v
src/FCF/Array.v
src/FCF/Asymptotic.v
src/FCF/Bernoulli.v
src/FCF/Blist.v
src/FCF/Class.v
src/FCF/Comp.v
src/FCF/CompFold.v
src/FCF/Crypto.v
src/FCF/DetSem.v
src/FCF/DiffieHellman.v
src/FCF/DistRules.v
src/FCF/DistSem.v
src/FCF/DistTacs.v
src/FCF/Encryption.v
src/FCF/Encryption_PK.v
src/FCF/Signature.v
src/FCF/EqDec.v
src/FCF/ExpectedPolyTime.v
src/FCF/FCF.v
src/FCF/Fold.v
src/FCF/GenTacs.v
src/FCF/GroupTheory.v
src/FCF/HasDups.v
src/FCF/Hybrid.v
src/FCF/Limit.v
src/FCF/Lognat.v
src/FCF/NoDup_gen.v
src/FCF/NotationV1.v
src/FCF/NotationV2.v
src/FCF/OTP.v
src/FCF/OracleCompFold.v
src/FCF/OracleHybrid.v
src/FCF/PRF.v
src/FCF/PRF_Convert.v
src/FCF/PRG.v
src/FCF/ProgTacs.v
src/FCF/ProgramLogic.v
src/FCF/Rat.v
src/FCF/RepeatCore.v
src/FCF/RndDup.v
src/FCF/RndGrpElem.v
src/FCF/RndInList.v
src/FCF/RndListElem.v
src/FCF/RndListPred.v
src/FCF/RndNat.v
src/FCF/RndPerm.v
src/FCF/ROM.v
src/FCF/SemEquiv.v
src/FCF/SplitVector.v
src/FCF/StdNat.v
src/FCF/Tactics.v
src/FCF/TwoWorldsEquiv.v
src/FCF/WC_PolyTime.v
src/FCF/WC_PolyTime_old.v
src/FCF/Broken/ConstructedFunc.v
src/FCF/Broken/Encryption_2W.v
src/FCF/Broken/ListHybrid.v
src/FCF/Broken/PRP_PRF.v
src/FCF/Broken/Procedure.v
src/FCF/Broken/RandPermSwitching.v
src/FCF/Broken/Sigma.v
src/FCF/Broken/State.v
src/FCF/examples/Commit.v
src/FCF/examples/EC_DRBG.v
src/FCF/examples/ElGamal.v
src/FCF/examples/PRF_DRBG.v
src/FCF/examples/PRF_Encryption_IND_CPA.v
src/HMAC/GHMAC_PRF.v
src/HMAC/GNMAC_PRF.v
src/HMAC/HMAC_PRF.v
src/HMAC/HMAC_spec.v
src/HMAC/Message.v
src/HMAC/NMAC_to_HMAC.v
src/HMAC/cAU.v
src/HMAC/hF.v