-R src Crypto
-R bbv/theories bbv
bbv/theories/BinNotation.v
bbv/theories/BinNotationZ.v
bbv/theories/DepEq.v
bbv/theories/DepEqNat.v
bbv/theories/HexNotation.v
bbv/theories/HexNotationWord.v
bbv/theories/HexNotationZ.v
bbv/theories/NLib.v
bbv/theories/N_Z_nat_conversions.v
bbv/theories/NatLib.v
bbv/theories/Nomega.v
bbv/theories/ReservedNotations.v
bbv/theories/Word.v
bbv/theories/WordScope.v
bbv/theories/ZHints.v
bbv/theories/ZLib.v
src/AbstractInterpretation.v
src/AbstractInterpretationProofs.v
src/AbstractInterpretationWf.v
src/AbstractInterpretationZRangeProofs.v
src/BoundsPipeline.v
src/CLI.v
src/COperationSpecifications.v
src/CStringification.v
src/CompilersTestCases.v
src/Demo.v
src/GENERATEDIdentifiersWithoutTypes.v
src/GENERATEDIdentifiersWithoutTypesProofs.v
src/Language.v
src/LanguageInversion.v
src/LanguageWf.v
src/MiscCompilerPasses.v
src/MiscCompilerPassesProofs.v
src/PreLanguage.v
src/Rewriter.v
src/RewriterAll.v
src/RewriterAllTactics.v
src/RewriterInterpProofs1.v
src/RewriterRules.v
src/RewriterRulesProofs.v
src/RewriterWf1.v
src/RewriterWf2.v
src/SlowPrimeSynthesisExamples.v
src/StandaloneHaskellMain.v
src/StandaloneOCamlMain.v
src/TAPSort.v
src/UnderLets.v
src/UnderLetsProofs.v
src/Algebra/Field.v
src/Algebra/Field_test.v
src/Algebra/Group.v
src/Algebra/Hierarchy.v
src/Algebra/IntegralDomain.v
src/Algebra/Monoid.v
src/Algebra/Nsatz.v
src/Algebra/Ring.v
src/Algebra/ScalarMult.v
src/Algebra/SubsetoidRing.v
src/Arithmetic/BarrettReduction.v
src/Arithmetic/BaseConversion.v
src/Arithmetic/Core.v
src/Arithmetic/FancyMontgomeryReduction.v
src/Arithmetic/Freeze.v
src/Arithmetic/ModOps.v
src/Arithmetic/ModularArithmeticPre.v
src/Arithmetic/ModularArithmeticTheorems.v
src/Arithmetic/Partition.v
src/Arithmetic/PrimeFieldTheorems.v
src/Arithmetic/Primitives.v
src/Arithmetic/Saturated.v
src/Arithmetic/UniformWeight.v
src/Arithmetic/WordByWordMontgomery.v
src/Arithmetic/BarrettReduction/Generalized.v
src/Arithmetic/BarrettReduction/HAC.v
src/Arithmetic/BarrettReduction/RidiculousFish.v
src/Arithmetic/BarrettReduction/Wikipedia.v
src/Arithmetic/MontgomeryReduction/Definition.v
src/Arithmetic/MontgomeryReduction/Proofs.v
src/Curves/Edwards/AffineProofs.v
src/Curves/Edwards/Pre.v
src/Curves/Edwards/XYZT/Basic.v
src/Curves/Edwards/XYZT/Precomputed.v
src/Curves/Montgomery/Affine.v
src/Curves/Montgomery/AffineInstances.v
src/Curves/Montgomery/AffineProofs.v
src/Curves/Montgomery/XZ.v
src/Curves/Montgomery/XZProofs.v
src/Curves/Weierstrass/Affine.v
src/Curves/Weierstrass/AffineProofs.v
src/Curves/Weierstrass/Jacobian.v
src/Curves/Weierstrass/Projective.v
src/Fancy/Barrett256.v
src/Fancy/Compiler.v
src/Fancy/Montgomery256.v
src/Fancy/Prod.v
src/Fancy/Spec.v
src/Primitives/EdDSARepChange.v
src/Primitives/MxDHRepChange.v
src/PushButtonSynthesis/BarrettReduction.v
src/PushButtonSynthesis/BarrettReductionReificationCache.v
src/PushButtonSynthesis/FancyMontgomeryReduction.v
src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
src/PushButtonSynthesis/InvertHighLow.v
src/PushButtonSynthesis/LegacySynthesisTactics.v
src/PushButtonSynthesis/Primitives.v
src/PushButtonSynthesis/ReificationCache.v
src/PushButtonSynthesis/SaturatedSolinas.v
src/PushButtonSynthesis/SaturatedSolinasReificationCache.v
src/PushButtonSynthesis/SmallExamples.v
src/PushButtonSynthesis/UnsaturatedSolinas.v
src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
src/PushButtonSynthesis/WordByWordMontgomery.v
src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v
src/Rewriter/Arith.v
src/Rewriter/ArithWithCasts.v
src/Rewriter/NBE.v
src/Rewriter/StripLiteralCasts.v
src/Rewriter/ToFancy.v
src/Rewriter/ToFancyWithCasts.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/Ed25519.v
src/Spec/EdDSA.v
src/Spec/ModularArithmetic.v
src/Spec/MontgomeryCurve.v
src/Spec/MxDH.v
src/Spec/WeierstrassCurve.v
src/Spec/Test/X25519.v
src/Util/AdditionChainExponentiation.v
src/Util/Arg.v
src/Util/AutoRewrite.v
src/Util/Bool.v
src/Util/BoundedWord.v
src/Util/CPSNotations.v
src/Util/CPSUtil.v
src/Util/ChangeInAll.v
src/Util/Comparison.v
src/Util/Curry.v
src/Util/Decidable.v
src/Util/DefaultedTypes.v
src/Util/Equality.v
src/Util/ErrorT.v
src/Util/Factorize.v
src/Util/FixCoqMistakes.v
src/Util/FixedWordSizes.v
src/Util/FixedWordSizesEquality.v
src/Util/FsatzAutoLemmas.v
src/Util/GlobalSettings.v
src/Util/HList.v
src/Util/HProp.v
src/Util/IdfunWithAlt.v
src/Util/IffT.v
src/Util/Isomorphism.v
src/Util/LetIn.v
src/Util/LetInMonad.v
src/Util/ListUtil.v
src/Util/Logic.v
src/Util/Loops.v
src/Util/NUtil.v
src/Util/NatUtil.v
src/Util/Notations.v
src/Util/NumTheoryUtil.v
src/Util/Option.v
src/Util/OptionList.v
src/Util/PER.v
src/Util/ParseTaps.v
src/Util/PartiallyReifiedProp.v
src/Util/Pointed.v
src/Util/PointedProp.v
src/Util/Pos.v
src/Util/PrimitiveHList.v
src/Util/PrimitiveProd.v
src/Util/PrimitiveSigma.v
src/Util/Prod.v
src/Util/QUtil.v
src/Util/Relations.v
src/Util/Sigma.v
src/Util/Sum.v
src/Util/Sumbool.v
src/Util/Tactics.v
src/Util/TagList.v
src/Util/Tower.v
src/Util/Tuple.v
src/Util/Unit.v
src/Util/WordUtil.v
src/Util/ZBounded.v
src/Util/ZRange.v
src/Util/ZUtil.v
src/Util/Bool/Equality.v
src/Util/Bool/IsTrue.v
src/Util/Bool/Reflect.v
src/Util/Decidable/Bool2Prop.v
src/Util/Decidable/Decidable2Bool.v
src/Util/FMapPositive/Equality.v
src/Util/ListUtil/FoldBool.v
src/Util/ListUtil/Forall.v
src/Util/ListUtil/ForallIn.v
src/Util/ListUtil/SetoidList.v
src/Util/Logic/ExistsEqAnd.v
src/Util/Logic/ImplAnd.v
src/Util/Logic/ProdForall.v
src/Util/MSetPositive/Equality.v
src/Util/MSetPositive/Facts.v
src/Util/NUtil/WithoutReferenceToZ.v
src/Util/SideConditions/AdmitPackage.v
src/Util/SideConditions/Autosolve.v
src/Util/SideConditions/CorePackages.v
src/Util/SideConditions/ModInvPackage.v
src/Util/SideConditions/ReductionPackages.v
src/Util/SideConditions/RingPackage.v
src/Util/Sigma/Associativity.v
src/Util/Sigma/Lift.v
src/Util/Sigma/MapProjections.v
src/Util/Sigma/Related.v
src/Util/Strings/Ascii.v
src/Util/Strings/BinaryString.v
src/Util/Strings/Decimal.v
src/Util/Strings/Equality.v
src/Util/Strings/HexString.v
src/Util/Strings/OctalString.v
src/Util/Strings/ParseArithmetic.v
src/Util/Strings/Show.v
src/Util/Strings/String.v
src/Util/Strings/StringMap.v
src/Util/Strings/String_as_OT.v
src/Util/Tactics/BreakMatch.v
src/Util/Tactics/CPSId.v
src/Util/Tactics/CacheTerm.v
src/Util/Tactics/ChangeInAll.v
src/Util/Tactics/ClearAll.v
src/Util/Tactics/ClearDuplicates.v
src/Util/Tactics/ClearbodyAll.v
src/Util/Tactics/ConstrFail.v
src/Util/Tactics/Contains.v
src/Util/Tactics/ConvoyDestruct.v
src/Util/Tactics/DebugPrint.v
src/Util/Tactics/DestructHead.v
src/Util/Tactics/DestructHyps.v
src/Util/Tactics/DestructTrivial.v
src/Util/Tactics/DoWithHyp.v
src/Util/Tactics/ESpecialize.v
src/Util/Tactics/ETransitivity.v
src/Util/Tactics/EvarExists.v
src/Util/Tactics/Forward.v
src/Util/Tactics/GetGoal.v
src/Util/Tactics/HasBody.v
src/Util/Tactics/Head.v
src/Util/Tactics/HeadUnderBinders.v
src/Util/Tactics/MoveLetIn.v
src/Util/Tactics/NormalizeCommutativeIdentifier.v
src/Util/Tactics/Not.v
src/Util/Tactics/OnSubterms.v
src/Util/Tactics/PoseTermWithName.v
src/Util/Tactics/PrintContext.v
src/Util/Tactics/Revert.v
src/Util/Tactics/RewriteHyp.v
src/Util/Tactics/RunTacticAsConstr.v
src/Util/Tactics/SetEvars.v
src/Util/Tactics/SetoidSubst.v
src/Util/Tactics/SideConditionsBeforeToAfter.v
src/Util/Tactics/SimplifyProjections.v
src/Util/Tactics/SimplifyRepeatedIfs.v
src/Util/Tactics/SpecializeAllWays.v
src/Util/Tactics/SpecializeBy.v
src/Util/Tactics/SplitInContext.v
src/Util/Tactics/SubstEvars.v
src/Util/Tactics/SubstLet.v
src/Util/Tactics/Test.v
src/Util/Tactics/TransparentAssert.v
src/Util/Tactics/UnfoldArg.v
src/Util/Tactics/UnifyAbstractReflexivity.v
src/Util/Tactics/UniquePose.v
src/Util/Tactics/VM.v
src/Util/ZRange/BasicLemmas.v
src/Util/ZRange/CornersMonotoneBounds.v
src/Util/ZRange/LandLorBounds.v
src/Util/ZRange/Operations.v
src/Util/ZRange/OperationsBounds.v
src/Util/ZRange/Show.v
src/Util/ZRange/SplitBounds.v
src/Util/ZUtil/AddGetCarry.v
src/Util/ZUtil/AddModulo.v
src/Util/ZUtil/CC.v
src/Util/ZUtil/CPS.v
src/Util/ZUtil/Combine.v
src/Util/ZUtil/Definitions.v
src/Util/ZUtil/DistrIf.v
src/Util/ZUtil/Div.v
src/Util/ZUtil/Divide.v
src/Util/ZUtil/EquivModulo.v
src/Util/ZUtil/Ge.v
src/Util/ZUtil/Hints.v
src/Util/ZUtil/Land.v
src/Util/ZUtil/LandLorBounds.v
src/Util/ZUtil/LandLorShiftBounds.v
src/Util/ZUtil/Le.v
src/Util/ZUtil/Lnot.v
src/Util/ZUtil/Log2.v
src/Util/ZUtil/ModInv.v
src/Util/ZUtil/Modulo.v
src/Util/ZUtil/Morphisms.v
src/Util/ZUtil/Mul.v
src/Util/ZUtil/MulSplit.v
src/Util/ZUtil/N2Z.v
src/Util/ZUtil/Notations.v
src/Util/ZUtil/Odd.v
src/Util/ZUtil/Ones.v
src/Util/ZUtil/Opp.v
src/Util/ZUtil/Peano.v
src/Util/ZUtil/Pow.v
src/Util/ZUtil/Pow2.v
src/Util/ZUtil/Pow2Mod.v
src/Util/ZUtil/Quot.v
src/Util/ZUtil/Rshi.v
src/Util/ZUtil/Sgn.v
src/Util/ZUtil/Shift.v
src/Util/ZUtil/Sorting.v
src/Util/ZUtil/Stabilization.v
src/Util/ZUtil/Tactics.v
src/Util/ZUtil/Testbit.v
src/Util/ZUtil/Z2Nat.v
src/Util/ZUtil/ZSimplify.v
src/Util/ZUtil/Zselect.v
src/Util/ZUtil/Div/Bootstrap.v
src/Util/ZUtil/Hints/Core.v
src/Util/ZUtil/Hints/PullPush.v
src/Util/ZUtil/Hints/ZArith.v
src/Util/ZUtil/Hints/Ztestbit.v
src/Util/ZUtil/Modulo/Bootstrap.v
src/Util/ZUtil/Modulo/PullPush.v
src/Util/ZUtil/Tactics/CompareToSgn.v
src/Util/ZUtil/Tactics/DivModToQuotRem.v
src/Util/ZUtil/Tactics/DivideExistsMul.v
src/Util/ZUtil/Tactics/LinearSubstitute.v
src/Util/ZUtil/Tactics/LtbToLt.v
src/Util/ZUtil/Tactics/PeelLe.v
src/Util/ZUtil/Tactics/PrimeBound.v
src/Util/ZUtil/Tactics/PullPush.v
src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
src/Util/ZUtil/Tactics/RewriteModSmall.v
src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
src/Util/ZUtil/Tactics/SplitMinMax.v
src/Util/ZUtil/Tactics/ZeroBounds.v
src/Util/ZUtil/Tactics/Ztestbit.v
src/Util/ZUtil/Tactics/PullPush/Modulo.v
src/Util/ZUtil/ZSimplify/Autogenerated.v
src/Util/ZUtil/ZSimplify/Core.v
src/Util/ZUtil/ZSimplify/Simple.v