ยซ Up

fiat-crypto 0.0.16 2 h 22 m ๐Ÿ†

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-findutils        1           Virtual package relying on findutils
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.16.1      Formal proof management system
dune                  3.12.1      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
authors: [
  "Andres Erbsen <andreser@mit.edu>"
  "Google Inc."
  "Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com>"
  "Massachusetts Institute of Technology"
  "Zoe Paraskevopoulou <zoe.paraskevopoulou@gmail.com>"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/fiat-crypto"
bug-reports: "https://github.com/mit-plv/fiat-crypto/issues"
license: "MIT OR Apache-2.0 OR BSD-1-Clause"
build: [
  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "BINDIR=%{bin}%" "install" "install-standalone-ocaml"]
depends: [
  "conf-findutils" {build}
  "ocaml" {build & >= "4.08~"}
  "ocamlfind" {build}
  "coq" {>= "8.15~"}
  "coq-coqprime" {>= "1.2.0"}
  "coq-rewriter" {>= "0.0.6" & <= "0.0.7"}
  "coq-rupicola" {= "0.0.6"}
  "coq-bedrock2-compiler" {= "0.0.4"}
]
conflict-class: [
  "coq-fiat-crypto"
]
dev-repo: "git+https://github.com/mit-plv/fiat-crypto.git"
synopsis: "Cryptographic Primitive Code Generation by Fiat"
description: """
Coq code and proofs for a command-line binary that can synthesize proven-correct
big-integer modular field arithmetic operations for cryptography.
Target languages include C, Rust, Zig, Go, and bedrock2.
"""
tags: ["logpath:Crypto"]
url {
  src: "https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.16.tar.gz"
  checksum: "sha512=db5e3ce6eb30066150c3611222c48f0eaab02f5b6101faab20d8a586c4f23bacb0c46372eff03736d7f017195500b3ea0203895052bf6ade752030a08c77e86d"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-fiat-crypto.0.0.16 coq.8.16.1
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-fiat-crypto.0.0.16 coq.8.16.1
Return code
0
Duration
1 h 4 m

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.16 coq.8.16.1
Return code
0
Duration
2 h 22 m

Installation size

Total: 354 M

  • 27 M ../ocaml-base-compiler.4.14.0/bin/word_by_word_montgomery
  • 25 M ../ocaml-base-compiler.4.14.0/bin/unsaturated_solinas
  • 23 M ../ocaml-base-compiler.4.14.0/bin/saturated_solinas
  • 23 M ../ocaml-base-compiler.4.14.0/bin/base_conversion
  • 15 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Syntax.vo
  • 13 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Symbolic.vo
  • 11 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie.vo
  • 6 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Field.glob
  • 5 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/Proofs.vo
  • 5 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/UnsaturatedSolinasHeuristics/Tests.vo
  • 5 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo
  • 5 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/AffineProofs.vo
  • 5 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapProd.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/EquivalenceProofs.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapOption.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/SymbolicProofs.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapSum.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ToFancyWithCasts.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p224_64_new.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/GarageDoor.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Ring.glob
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ArithWithCasts.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/NBE.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/Wf.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersGENERATED.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Projective.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/Field25519.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Compiler.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p224_64.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p256_64.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrieEx.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/X25519_64.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/EdwardsMontgomery.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/MultiRetSplit.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/Arith.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Spec.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/EquivalenceProofs.glob
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/MulSplit.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/XZProofs.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/ZRangeProofs.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/X1305_32.vo
  • 1019 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Equivalence.vo
  • 1009 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FsatzAutoLemmas.vo
  • 992 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Expr.vo
  • 983 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapFacts.vo
  • 958 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo
  • 938 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Symbolic.glob
  • 934 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/RulesProofs.vo
  • 921 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie.glob
  • 913 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/Proofs.glob
  • 900 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapProd.glob
  • 843 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/Proofs.vo
  • 841 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Prod.vo
  • 828 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapBool.vo
  • 818 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Barrett256.vo
  • 815 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil.vo
  • 808 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Expr.vo
  • 797 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/PerfTesting/Core.vo
  • 794 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo
  • 722 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/Wf.glob
  • 679 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/IR.vo
  • 649 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/Poly1305/Field1305.vo
  • 648 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/InversionExtra.vo
  • 647 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/LoadStoreList.vo
  • 642 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/MontgomeryLadder.vo
  • 627 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/LadderStep.vo
  • 620 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Sum.vo
  • 619 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo
  • 619 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo
  • 605 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/Proofs.glob
  • 604 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Low.vo
  • 595 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo
  • 590 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/WordByWordMontgomery.vo
  • 573 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Low.glob
  • 568 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/List.vo
  • 567 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Jacobian.vo
  • 564 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf2.vo
  • 562 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil.glob
  • 555 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/LoadStoreList.glob
  • 543 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapN.vo
  • 542 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapZ.vo
  • 539 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersBasicGENERATED.vo
  • 528 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Rules.glob
  • 527 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Cmd.vo
  • 511 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Language.vo
  • 506 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo
  • 502 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/UnsaturatedSolinas.vo
  • 492 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/IR.glob
  • 490 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Language.glob
  • 489 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/Primitives.vo
  • 488 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo
  • 488 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CLI.vo
  • 480 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/SymbolicProofs.glob
  • 465 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Option.vo
  • 461 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo
  • 453 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Func.vo
  • 447 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/WordByWordMontgomery.glob
  • 446 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/ZRangeProofs.glob
  • 442 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Montgomery256.vo
  • 434 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapSect.vo
  • 428 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/LandLorBounds.vo
  • 428 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/Signature.vo
  • 419 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Bool.vo
  • 412 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Unit.vo
  • 411 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Empty.vo
  • 409 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Compiler.glob
  • 397 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/WordByWordMontgomery.vo
  • 384 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Demo.vo
  • 381 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetSum.vo
  • 379 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/BoundsPipeline.vo
  • 372 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Rules.vo
  • 361 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Equivalence.glob
  • 348 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/AffineProofs.vo
  • 334 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/WordByWordMontgomery.vo
  • 325 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo
  • 325 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ArithmeticShiftr.vo
  • 315 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Core.vo
  • 314 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tuple.vo
  • 301 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/GarageDoor.glob
  • 298 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/StringMap.vo
  • 298 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Freeze.vo
  • 292 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BYInv.glob
  • 292 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BYInv.vo
  • 291 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/WordByWordMontgomery.glob
  • 281 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Forall.vo
  • 279 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/AbstractInterpretation.vo
  • 277 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Saturated.vo
  • 271 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/AdditionChains.vo
  • 271 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Jacobian.glob
  • 270 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf1.vo
  • 269 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo
  • 268 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Flip.vo
  • 267 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo
  • 267 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Core.glob
  • 264 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/SlowPrimeSynthesisExamples.glob
  • 261 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders.vo
  • 261 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/UnsaturatedSolinas.glob
  • 258 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo
  • 258 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction.vo
  • 255 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersGENERATEDProofs.vo
  • 255 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Autogenerated.glob
  • 254 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Util.vo
  • 253 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Sum.vo
  • 251 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/CSwap.vo
  • 250 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/SlowPrimeSynthesisExamples.v
  • 249 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CastLemmas.glob
  • 246 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/XYZT/Basic.vo
  • 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/RulesProofs.glob
  • 239 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/MontgomeryLadder.vo
  • 238 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/TableMult/TableMult.glob
  • 237 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/AffineProofs.vo
  • 235 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapIso.vo
  • 232 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/StdlibCompat.vo
  • 232 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/ZRange.vo
  • 231 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Prod.vo
  • 230 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Autogenerated.vo
  • 229 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BarrettReductionReificationCache.vo
  • 229 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v
  • 226 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Broadcast.vo
  • 225 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tuple.glob
  • 223 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BYInversionReificationCache.vo
  • 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo
  • 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Option.vo
  • 219 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo
  • 217 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/ZRange.glob
  • 217 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/AddAssocLeft.vo
  • 216 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/TableMult/TableMult.vo
  • 215 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapFlip.vo
  • 212 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Saturated.glob
  • 209 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/OrdersEx.vo
  • 206 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Arg.vo
  • 206 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/Primitives.glob
  • 206 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/XZProofs.glob
  • 205 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Equivalence.vo
  • 204 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/FlattenThunkedRects.vo
  • 204 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Prod.vo
  • 203 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.v
  • 203 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CompilersTestCases.glob
  • 202 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CLI.glob
  • 200 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Cmd.vo
  • 200 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/CornersMonotoneBounds.vo
  • 197 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/LadderStep.vo
  • 195 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo
  • 194 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo
  • 192 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapUnit.vo
  • 189 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/COperationSpecifications.glob
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie/ShapeEx.vo
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Interface/Compilation2.vo
  • 186 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/BoundsPipeline.glob
  • 186 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/LoadStoreList.vo
  • 185 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/StdlibCompat.glob
  • 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/StripLiteralCasts.vo
  • 183 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo
  • 183 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders.glob
  • 182 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/MontgomeryLadderProperties.vo
  • 182 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Iso.vo
  • 181 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf2.glob
  • 180 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetIso.vo
  • 177 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/BasicLemmas.vo
  • 176 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MakeAccessSizes.vo
  • 175 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/UnfoldValueBarrier.vo
  • 175 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BaseConversion.vo
  • 174 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/EquivalenceProofs.v
  • 174 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/Proofs.v
  • 172 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/Stringification.vo
  • 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.glob
  • 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf.vo
  • 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SaturatedSolinasReificationCache.vo
  • 169 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo
  • 168 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ModInv.vo
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/Reflect.vo
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction.glob
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Go.vo
  • 166 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/COperationSpecifications.vo
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Testbit.glob
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Specs/Field.vo
  • 163 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/ParseArithmetic.glob
  • 163 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.v
  • 162 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Flatten.vo
  • 162 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/AbstractInterpretation.glob
  • 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ToFancy.vo
  • 157 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse.vo
  • 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/BaseConversion.vo
  • 155 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Func.glob
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/LandLorBounds.glob
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NatUtil.vo
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Names/MakeNames.vo
  • 153 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/CPSUtil.vo
  • 153 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BarrettReduction.vo
  • 152 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/Signature.glob
  • 151 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/EncodeDecode.vo
  • 151 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/List.vo
  • 150 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.glob
  • 150 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Util.glob
  • 149 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v
  • 149 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Derive.vo
  • 149 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/SlowPrimeSynthesisExamples.vo
  • 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LandLorBounds.vo
  • 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Symbolic.v
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/CPSUtil.glob
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Forall.glob
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.glob
  • 145 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.v
  • 145 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/FancyMontgomeryReduction.vo
  • 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Types.vo
  • 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/MulTwice.vo
  • 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SaturatedSolinas.vo
  • 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/Test.vo
  • 140 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/ParseArithmetic.vo
  • 138 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo
  • 138 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapOption.glob
  • 137 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/C.vo
  • 137 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Primitives/MxDHRepChange.vo
  • 136 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.glob
  • 136 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Operation.vo
  • 135 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Div.vo
  • 135 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetSum.glob
  • 132 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapSum.glob
  • 131 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/Semantics.glob
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Saturated.vo
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Facts.vo
  • 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.glob
  • 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ModInv.glob
  • 125 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Tactics.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Zig.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Field_test.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/UsedVarnames.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/RidiculousFish.glob
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.glob
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/WordByWordMontgomery.glob
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.glob
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/NamingConventions.vo
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Prod.glob
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie/Shape.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil.v
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Bool.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/RidiculousFish.vo
  • 121 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Arg.glob
  • 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/C.glob
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.glob
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Unit.vo
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Go.glob
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LandLorShiftBounds.vo
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BaseConversionReificationCache.vo
  • 118 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Empty.vo
  • 118 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/SplitRangeBounds.vo
  • 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/APINotations.vo
  • 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CastLemmas.vo
  • 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/UnsaturatedSolinasHeuristics.vo
  • 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FsatzAutoLemmas.glob
  • 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/JSON.vo
  • 115 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.glob
  • 115 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Expr.glob
  • 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Rust.vo
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Iso.vo
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/Semantics.vo
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Ring.vo
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/ScalarMult.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Bignum.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Java.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/Generalized.vo
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable.vo
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Div.glob
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/CornersMonotoneBounds.glob
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.glob
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf1.glob
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/CSwap.glob
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.vo
  • 106 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneOCamlMain.vo
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Sum.glob
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapSect.glob
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/ComputedOp.vo
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Func.vo
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Equality.vo
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ones.glob
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/MontgomeryReduction/Proofs.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/VarnameSet.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Flatten.glob
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Bitwise.vo
  • 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPassesProofs.vo
  • 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Standalone/StandaloneOCamlMain.vo
  • 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Standalone/StandaloneHaskellMain.vo
  • 100 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/PerfTesting/StandaloneOCamlMain.vo
  • 100 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MaxBounds.vo
  • 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Syntax.glob
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/Proofs.v
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Broadcast.glob
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT/List.vo
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.glob
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/IR.v
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneHaskellMain.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie.v
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse.glob
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/PrimeFieldTheorems.vo
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/Reflect.glob
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/AdditionChains.glob
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sum.vo
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/List.glob
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModOps.vo
  • 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Equality.vo
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie/ShapeEx.glob
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModularArithmeticTheorems.vo
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.v
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf.glob
  • 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Low.v
  • 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/Tactics.vo
  • 90 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/ByteBounds.vo
  • 90 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/JSON.glob
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/API.vo
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Language.v
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/QUtil.vo
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Freeze.vo
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Tactics.vo
  • 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/OptionList.vo
  • 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Rust.glob
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PartiallyReifiedProp.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/Pre.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Core.vo
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults.vo
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Field.vo
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetN.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults64.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Loops.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/FE310.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults32.vo
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/IntegralDomain.glob
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/FancyMontgomeryReduction.vo
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BaseConversion.vo
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Flatten.vo
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneDebuggingExamples.vo
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LandLorShiftBounds.glob
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModularArithmeticTheorems.glob
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Show.vo
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapEmpty.vo
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/ModOps.vo
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Zig.glob
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Option.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Interface/Representation.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/EdwardsMontgomery.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Testbit.vo
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Spec.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/MontgomeryLadder.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Option.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/TwosComplement.vo
  • 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Level.vo
  • 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Core.glob
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/PerfTesting/Core.glob
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Java.glob
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/MontgomeryReduction/Proofs.glob
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/Wf.v
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/BasicLemmas.glob
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/ScalarMult.glob
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapIso.glob
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.glob
  • 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/Point.vo
  • 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SmallExamples.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifierParameters.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NumTheoryUtil.vo
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Prod.glob
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Quot.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ones.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Rules.v
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/FlattenVarData.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Hierarchy.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetIso.glob
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NatUtil.glob
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapFacts.glob
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/UniformWeight.vo
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Equivalence.v
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie/Shape.glob
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma.glob
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CompilersTestCases.vo
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/WfExtra.vo
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/SplitBounds.vo
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Equality.glob
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Show.vo
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BaseConversion.glob
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Loops.glob
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/BoundsPipeline.v
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/SubsetoidRing.vo
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/Generalized.glob
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/HList.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable/Decidable2Bool.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/AffineProofs.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/Primitives.v
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapUnit.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/EquivalenceProperties.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Specs/Group.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapBool.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/PrimeFieldTheorems.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String_as_OT_old.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Flip.glob
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/WordByWordMontgomery.v
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MakeListLengths.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Specs/Field.glob
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Prod.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/HAC.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Freeze.glob
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/Operations.glob
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/UnsaturatedSolinasHeuristics.glob
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/MontgomeryCurve.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/APINotations.glob
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Compiler.v
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/ScalarMult.vo
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Saturated.glob
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/SymbolicProofs.v
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CLI.v
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/SubsetoidRing.glob
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/LoadStoreListVarData.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Show.glob
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Option.glob
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BaseConversion.glob
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/Affine.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/WeierstrassCurve.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Parse/Common.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/Curve25519.glob
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Spec.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Cmd.glob
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZBounded.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/Operations.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Parse/Common.glob
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/TruncatingShiftl.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/LadderStep.glob
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Group.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/MontgomeryLadder.glob
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/XZ.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NumTheoryUtil.glob
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Primitives.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LandLorBounds.glob
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/IntegralDomain.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Stabilization.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Sum.glob
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/AdditionChainExponentiation.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModOps.glob
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/StdlibCompat.v
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/WordByWordMontgomery.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Partition.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/GarageDoor.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Core.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Names/MakeNames.glob
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/XYZT/Precomputed.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/CC.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BYInv.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/PullPush.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Saturated.v
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/All.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Barrett256.glob
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidList.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/UnderLetsProofsExtra.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.glob
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/AddGetCarry.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/AffineInstances.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/Test/X25519.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/ReificationCache.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.glob
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/CPS.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapProd.v
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Listable.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Interface/Compilation2.glob
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidListFlatMap.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/GroupAllBy.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo/PullPush.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPasses.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/FMapPositive/Equality.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/Signature.v
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPassesProofsExtra.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/Wikipedia.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/HAC.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/PreExtra.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String_as_OT.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/WordByWordMontgomery.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/FLia.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/OnesFrom.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/UnsaturatedSolinas.v
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/ZRangeProofs.v
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/WfExtra.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BarrettReduction.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/Curve25519.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModularArithmeticPre.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MakeAccessSizes.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Instances.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Montgomery256.glob
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.glob
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/RulesProofs.v
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo/PullPush.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/XZ.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapEmpty.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Nsatz.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tuple.v
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveProd.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Iso.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Rshi.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/ZRange.v
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/Stringification.glob
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifierParameters.glob
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/UniformWeight.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow2Mod.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/OperationsBounds.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/TwosComplement.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/Show.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapInterface.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/NamingConventions.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf2.v
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Prod.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Bitwise.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveSigma.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/LoadStoreList.v
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Core.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Types.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Simple.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/LadderStep.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SimplifyFractionsLe.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Demo.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Prod.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/TableMult/TableMult.v
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Definitions.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sorting/Sorted/Proper.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Primitives/MxDHRepChange.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ltz.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/Loops.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SmallExamples.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/AllTacticsExtra.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPassesProofs.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/FoldBool.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Projective.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Land.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/SignBit.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/MontgomeryLadderProperties.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sum.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/ModularArithmetic.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/PerfTesting/Core.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/OptionList.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveSigma.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Iso.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Equality.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Quot.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SolveTestbit.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Group.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Field_test.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/CPS.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/EquivModulo.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Log2.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/FancyMontgomeryReduction.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/CompleteEdwardsCurve.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Util.v
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Definitions.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PullPush/Modulo.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SolveRange.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/C.v
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PointedProp.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/ZArith.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Equality.glob
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Equivalence.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Sorting.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/LtbToLt.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Permutation.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidList.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Autogenerated.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/UsedVarnames.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Expr.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Bool.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModularArithmeticPre.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Empty.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/IdfunWithAlt.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/ReplaceNegWithPos.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Go.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/LoadStoreList.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/AbstractInterpretation.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Unit.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable/Bool2Prop.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Divide.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/TestRules.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Peano.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/ReductionPackages.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/List.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Le.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Equality.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Project.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Combine.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/MontgomeryReduction/Definition.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapSect.v
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT/List.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/PreExtra.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Jacobian.v
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf1.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/FancyMontgomeryReduction.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/ZeroBounds.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Derive.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Affine.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT/Show.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/ScalarMult.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Expr.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/ParseArithmeticToTaps.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Superscript.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SaturatedSolinas.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/COperationSpecifications.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Wf.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Option.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/OrdersEx.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveProd.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/LinearSubstitute.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/ParseArithmetic.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/TestRulesProofs.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String_as_OT_old.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Func.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Core.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/TAPSort.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/RewriteModSmall.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lor.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/Sorting.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Factorize.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Sorting.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/LetInMonad.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapFlip.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Equality.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapOption.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lxor.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/XYZT/Basic.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/APINotations.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PeelLe.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Monoid.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/EncodeDecode.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapSum.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Names/VarnameGenerator.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/TestAsm.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/Pre.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPasses.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Notations.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Partition.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/DistrIf.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/WordByWordMontgomeryReificationCache.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/N2Z.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/CPSUtil.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/Reflect.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/WithoutReferenceToZ.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/Testbit.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/ModInvPackage.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/Ztestbit.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Filter.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/MulSplit.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Subscript.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Simple.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidListRev.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetSum.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/Autosolve.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Prod.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Z2Nat.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/Show.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/HList.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Core.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Arg.v
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable/Decidable2Bool.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/DivModToQuotRem.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/MxDH.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Rust.v
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Stabilization.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/Core.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/Ztestbit.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Odd.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/InvertHighLow.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Cmd.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZBounded.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/MontgomeryEquivalence.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/FoldBool.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Decimal.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/AddGetCarry.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/RingPackage.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/WordByWordMontgomery.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/List.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SplitMinMax.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/MxDH.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Primitives.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Partition.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Zselect.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneOCamlMain.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow2.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Java.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Nat2Z.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Cmd.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Sgn.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ArithmeticShiftr.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/AdditionChains.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapIso.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo/Bootstrap.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/Zig.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ModExp.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PartiallyReifiedProp.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/CornersMonotoneBounds.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie/ShapeEx.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/XZProofs.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/Wikipedia.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Bignum.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/AddModulo.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Opp.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RewriteHyp.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ge.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/InversionExtra.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LnotModulo.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/PermutationCompat.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/UnsaturatedSolinasReificationCache.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lnot.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Lift.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/QUtil.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/DivideExistsMul.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Div/Bootstrap.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/TagList.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/CSwap.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Mul.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Stringification/JSON.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PointedProp.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Broadcast.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ModInv.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Ascii.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Forall.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/IndexOf.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Sum.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PullPush.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/CompareToSgn.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Instances.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Hierarchy.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidListFlatMap.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Ring.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PrimeBound.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Relations.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Option.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/XYZT/Precomputed.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Loops.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Related.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NatUtil.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MaxBounds.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/UnsaturatedSolinasHeuristics/Tests.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/ModOps.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Spec.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String_as_OT.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/UnsaturatedSolinasHeuristics.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Operation.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/WithBedrock/Semantics.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Level.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/ReductionPackages.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Land.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/MulTwice.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/ForallIn.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/NthExt.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Monoid.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/Affine.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapFacts.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/ParseArithmeticToTaps.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneDebuggingExamples.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BaseConversion.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Div.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LandLorShiftBounds.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetIso.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CompilersTestCases.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/BasicLemmas.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/BreakMatch.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Pointed.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Core.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ParseTaps.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Permutation.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BaseConversion.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/HProp.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/AffineProofs.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrie/Shape.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sumbool.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LandLorBounds.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Equality.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Show.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Related.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Prod.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Tactics.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/MontgomeryCurve.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SetoidSubst.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/OperationsBounds.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sorting/Sorted/Proper.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Option.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/ByteBounds.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Freeze.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p224_64_new.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Barrett256.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/TruncatingShiftl.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/AffineProofs.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeUnderBindersBy.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Flip.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModularArithmeticTheorems.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Interface/Compilation2.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Superscript.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/WeierstrassCurve.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneHaskellMain.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/GroupAllBy.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/RidiculousFish.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/AutoRewrite.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/DynList.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructHead.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Listable.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Empty.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Bool.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/SplitRangeBounds.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/ScalarMult.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/PrimeFieldTheorems.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/SplitBounds.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Unit.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/WfExtra.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/LetIn.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Project.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Montgomery256.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DebugPrint.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/ModularArithmetic.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/PerfTesting/StandaloneOCamlMain.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Freeze.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MakeAccessSizes.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/BaseConversion.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveHList.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Comparison.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/LetInMonad.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Notations.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PullPush/Modulo.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/MontgomeryReduction/Proofs.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NumTheoryUtil.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Names/MakeNames.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/EquivModulo.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/CompleteEdwardsCurve.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/InHypUnderBindersDo.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/MontgomeryReduction/Definition.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/FlattenVarData.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Notations.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Types.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/MontgomeryLadder.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Testbit.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ltz.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModOps.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Relations.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/Stringification.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Field.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapBool.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Saturated.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/EdwardsMontgomery.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Tactics.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Flatten.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FsatzAutoLemmas.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Specs/Field.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ExistsEqAnd.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/ReplaceNegWithPos.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Peano.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/FLia.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Factorize.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/LandLorBounds.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Rshi.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/IdfunWithAlt.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Syntax.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Pointed.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Flatten.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Parse/Common.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Func.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tower.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Func.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ones.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/TestRules.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tower.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/FoldMap.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CacheTerm.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FixCoqMistakes.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/SignBit.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Specs/Group.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/AffineInstances.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SaturatedSolinas.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BarrettReduction.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MakeListLengths.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AllInstances.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Bitwise.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Prod.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/Operations.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapUnit.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Log2.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Split.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/CombineExtend.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Le.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/CC.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Demo.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Empty.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetN.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/Generalized.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Nsatz.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Bool.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/NamingConventions.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/Field25519.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Unit.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Tactics.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SimplifyFractionsLe.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveSigma.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AllSuccesses.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/LadderStep.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Expr.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sum.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPassesProofs.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/CorePackages.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable/Bool2Prop.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Concat.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Prod.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/RemoveN.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Equality.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/LinearSubstitute.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/MontgomeryLadder.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ExistsEqAnd.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Names/VarnameGenerator.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/CastLemmas.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/FancyMontgomeryReduction.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneOCamlMain.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow2Mod.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Sum.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Lift.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/CorePackages.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapEmpty.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/AdditionChainExponentiation.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/DistrIf.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Projective.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/ModOps.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/MoveLetIn.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Orders/Iso.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/Equality.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneDebuggingExamples.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/WithoutReferenceToZ.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/HAC.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Subscript.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/UniformWeight.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Core.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifierParameters.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Primitives/MxDHRepChange.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Compose.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/LtbToLt.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/IntegralDomain.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/Equivalence.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Iso.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveProd.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Operation.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/OptionList.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ToFancyWithCasts.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/UsedVarnames.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Fancy/Spec.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable/Decidable2Bool.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT/List.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Equality.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Option.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo/PullPush.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Group.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidList.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/MontgomeryReduction/Definition.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Interface/Representation.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PointedProp.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/EncodeDecode.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/ScalarMult.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/List.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapFlip.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PeelLe.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/SubsetoidRing.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RewriteHyp.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPasses.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/OrdersEx.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/LetIn.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/Loops.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/CPS.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/VarnameSet.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SplitInContext.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String_as_OT_old.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/PreExtra.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/LoadStoreList.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/AffineProofs.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CPSId.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SolveRange.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p224_64_new.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/Poly1305/Field1305.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/CPSNotations.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/BaseConversion.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sumbool.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/PullPush.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/N2Z.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Derive.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Nsatz.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/IffT.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ToFancy.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/TagList.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/ReifiedOperation.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/ForallIn.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Core.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/TwosComplement.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructHyps.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Telescope/Instances.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/NBE.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Curry.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Partition.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PartiallyReifiedProp.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Definitions.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Hierarchy.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/UnderLetsProofsExtra.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/ReductionPackages.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/X25519_64.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/XYZT/Basic.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/XZ.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/X25519/Field25519.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SmallExamples.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/UnsaturatedSolinasHeuristics/Tests.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZBounded.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/MulSplit.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/FancyMontgomeryReduction.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Z2Nat.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MaxBounds.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SimplifyProjections.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SolveTestbit.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Stabilization.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/FoldBool.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/HList.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/HProp.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/FE310.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Partition.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults64.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults32.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/LadderStep.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Divide.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/Test.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Standalone/StandaloneHaskellMain.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/QUtil.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ParseTaps.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeUnderBindersBy.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Permutation.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/WfExtra.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Associativity.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeBy.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/Primitives.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Combine.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Decimal.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Standalone/StandaloneOCamlMain.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Ascii.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/RewriteModSmall.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/BarrettReduction/Wikipedia.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/FlattenThunkedRects.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/FoldMap.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/ByteBounds.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/AddGetCarry.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/MultiRetSplit.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Generic/Bignum.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/StripLiteralCasts.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/BreakMatch.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Level.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ETransitivity.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/Core.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/UnfoldValueBarrier.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/ZeroBounds.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/StandaloneHaskellMain.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/ModularArithmeticPre.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ArithWithCasts.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/MulTwice.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT/Show.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SimplifyFractionsLe.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Isomorphism.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/LoadStoreListVarData.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/MulSplit.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BYInversionReificationCache.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Listable.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HeadUnderBinders.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PER.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CountBinders.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Simple.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ConvoyDestruct.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/AddAssocLeft.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/CPSNotations.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/InvertHighLow.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructHead.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/VM.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/IndexOf.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Empty.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UniquePose.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/Arith.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UnifyAbstractReflexivity.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ArithmeticShiftr.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/TestAsm.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Unit.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveHList.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Cmd.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Bool.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/MxDH.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Filter.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ModExp.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Curry.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/InHypUnderBindersDo.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Quot.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/GroupAllBy.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/API.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Func.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/AutoRewrite.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/EquivModulo.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo/Bootstrap.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/SplitRangeBounds.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Compose.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Facts.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Odd.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Tactics.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/FindHyp.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/PullPush.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/Poly1305/Field1305.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/InversionExtra.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/PermutationCompat.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DoWithHyp.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Field_test.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HeadConstrEq.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/Forall.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/SplitBounds.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/GeneralizeOverHoles.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lor.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/ParseArithmeticToTaps.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ProdForall.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Forward.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/API.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PullPush/Modulo.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/ArithmeticCPS/Freeze.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/OperationsBounds.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SimplifyRepeatedIfs.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/String_as_OT.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RunTacticAsConstr.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidListRev.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/AffineProofs.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities/Project.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Peano.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FixCoqMistakes.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DebugPrint.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/AutoRewrite.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FixCoqMistakes.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/NormalizeCommutativeIdentifier.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/Exists.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Affine.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/InHypUnderBindersDo.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/FMapPositive/Equality.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/TagList.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/LeCompat.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/ModularArithmetic.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AppendUnderscores.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/OnesFrom.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/LetInMonad.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeUnderBindersBy.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/End2End/RupicolaCrypto/Spec.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FueledLUB.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/CC.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lxor.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/Test/X25519.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPassesProofsExtra.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Flatten.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SideConditionsBeforeToAfter.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/XYZT/Precomputed.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Land.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeAllWays.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/FlattenVarData.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearHead.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/ComputedOp.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/MapProjections.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Assembly/Parse/TestAsm.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/ReificationCache.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/TruncatingShiftl.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/TransparentAssert.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/IdfunWithAlt.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UnfoldArg.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Log2.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RevertUntil.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/Curve25519.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CacheTerm.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Associativity.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Algebra/Monoid.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Head.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/PerfTesting/StandaloneOCamlMain.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Pointed.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Unit.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Arithmetic/FLia.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BYInversionReificationCache.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/WeierstrassCurve.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Related.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Beta1.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Zeta1.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/Affine.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SetoidSubst.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/HProp.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/LinearSubstitute.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SetoidSubst.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PrintContext.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/CombineExtend.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sorting/Sorted/Proper.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Factorize.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/DefaultedTypes.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/X25519_64.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearFree.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Relations.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/All.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/ReifiedOperation.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/Point.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/ReplaceNegWithPos.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/LetIn.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SolveRange.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/MontgomeryCurve.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/Testbit.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SaturatedSolinasReificationCache.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Decidable/Bool2Prop.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DebugPrint.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Delta1.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/LtbToLt.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/UnderLetsProofsExtra.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SolveTestbit.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetN.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/X1305_32.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Interface/Representation.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PoseTermWithName.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Pos.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidListFlatMap.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/RewriteModSmall.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/TestRules.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/NthExt.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Names/VarnameGenerator.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow2.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/WarnIfGoalsRemain.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/IsTrue.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ImplAnd.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/MoveLetIn.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ChangeInAll.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/AffineProofs.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sumbool.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Common/Arrays/MakeListLengths.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow2Mod.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructTrivial.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ToFancyWithCasts.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/MoveLetIn.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/DivModToQuotRem.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/DistrIf.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PrintGoal.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FueledLUB.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearDuplicates.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Revert.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ConstrFail.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/EvarExists.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/CPSNotations.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Montgomery/AffineInstances.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/DivModToQuotRem.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UnifyAbstractReflexivity.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Le.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Contains.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Edwards/Pre.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BarrettReductionReificationCache.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/SignBit.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Standalone/StandaloneOCamlMain.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/CompleteEdwardsCurve.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/Sorting.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/Forall.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Specs/Group.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/FE310.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CPSId.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Lift.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Proofs/VarnameSet.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/Test.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/MapProjections.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Standalone/StandaloneHaskellMain.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SubstEvars.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Not.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults64.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ToFancy.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/EvarNormalize.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Translation/Parameters/Defaults32.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SetEvars.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Test.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/NBE.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/N2Z.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p256_64.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Rshi.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Sorting.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/OnSubterms.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearbodyAll.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearAll.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SubstLet.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ESpecialize.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PeelLe.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Partition.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tower.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HasBody.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/ReificationCache.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/WfExtra.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/FlattenThunkedRects.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/Show.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructHyps.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/ZeroBounds.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/MultiRetSplit.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/StripLiteralCasts.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/GetGoal.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/UnfoldValueBarrier.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/Loops.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/CorePackages.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Group/Point.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/All.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p224_64.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ProdForall.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/MiscCompilerPassesProofsExtra.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/ArithWithCasts.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/WithoutReferenceToZ.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/RingPackage.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ge.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Superscript.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/MulSplit.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PER.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ltz.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/AddAssocLeft.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SplitInContext.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Decimal.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/GlobalSettings.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersBasicGENERATED.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/Passes/Arith.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/TAPSort.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersGENERATEDProofs.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/IndexOf.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SplitInContext.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Z2Nat.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lnot.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SplitMinMax.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Nat2Z.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/Tactics.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Sorting.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/MulSplit.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ExistsEqAnd.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/SplitMinMax.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Facts.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Combine.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ParseTaps.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/RingPackage.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/LeCompat.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/ForallIn.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/DynList.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Spec/Test/X25519.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CPSId.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/RemoveN.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Divide.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SimplifyProjections.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BarrettReductionReificationCache.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapZ.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/PermutationCompat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/Exists.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Isomorphism.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/AllTacticsExtra.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Subscript.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/AbstractInterpretation/WfExtra.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeBy.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Filter.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BaseConversionReificationCache.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Isomorphism.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p256_64.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Equality.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/InvertHighLow.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/SaturatedSolinasReificationCache.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/p224_64.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/ModInvPackage.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ErrorT/Show.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/VM.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersGENERATED.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/AddModulo.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrieEx.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Examples/X1305_32.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/Ztestbit.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/AdditionChainExponentiation.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/AllTacticsExtra.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Opp.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AllInstances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/DivideExistsMul.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UniquePose.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/DynList.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructHead.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Ascii.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Odd.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/SetoidListRev.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Compose.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/ZArith.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Zselect.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/PushButtonSynthesis/BaseConversionReificationCache.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapN.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/Associativity.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ConvoyDestruct.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Structures/Equalities.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/NthExt.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/IffT.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/Specialized/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/BreakMatch.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo/Bootstrap.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ImplAnd.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Stringification/LoadStoreListVarData.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/Show.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Split.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Pos.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/FMapPositive/Equality.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Bedrock/Field/Synthesis/New/ComputedOp.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/ModInvPackage.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapInterface.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/FindHyp.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/GlobalSettings.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ETransitivity.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lxor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersGENERATEDProofs.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Mul.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersBasicGENERATED.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/Autosolve.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Show.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Concat.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Sgn.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/IsTrue.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapZ.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HeadUnderBinders.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Forward.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ModExp.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SideConditionsBeforeToAfter.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Curry.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/OnesFrom.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/FoldMap.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/TransparentAssert.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Sorting.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/ZArith.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SimplifyProjections.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PrimitiveHList.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Div/Bootstrap.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/Ztestbit.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RunTacticAsConstr.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CountBinders.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Curves/Weierstrass/Affine.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/PER.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Nat2Z.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/Testbit.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapN.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/Ztestbit.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/NUtil/Sorting.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LnotModulo.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SimplifyRepeatedIfs.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Language/IdentifiersGENERATED.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/NormalizeCommutativeIdentifier.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Pow2.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CacheTerm.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/Sorting.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UnfoldArg.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DoWithHyp.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/Ztestbit.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapTrieEx.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/TestRulesProofs.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/Show.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AllSuccesses.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/CombineExtend.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Equality.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/DivideExistsMul.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/DefaultedTypes.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/TAPSort.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/IffT.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Zselect.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ConstrFail.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HeadUnderBinders.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/CompareToSgn.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/LeCompat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Rewriter/TestRulesProofs.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Notations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Div/Bootstrap.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/MSets/MSetPositive/Show.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PrintContext.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FSets/FMapInterface.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Ge.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ConvoyDestruct.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearFree.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/StringMap.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Opp.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Lnot.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/RemoveN.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Zeta1.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/CountBinders.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Beta1.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AppendUnderscores.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AppendUnderscores.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PrimeBound.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Revert.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HeadConstrEq.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/SideConditions/Autosolve.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Sgn.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ChangeInAll.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/FueledLUB.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZRange/Show.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Unit.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeBy.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SimplifyRepeatedIfs.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/Forall.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UnifyAbstractReflexivity.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Sigma/MapProjections.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/CompareToSgn.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Concat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RunTacticAsConstr.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PoseTermWithName.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RevertUntil.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ListUtil/Split.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AllSuccesses.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/AddModulo.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Contains.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/GeneralizeOverHoles.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Unit.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearHead.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/VM.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/AllInstances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeAllWays.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Not.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/WarnIfGoalsRemain.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Head.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PrintGoal.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/OnSubterms.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructTrivial.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Test.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Pos.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/LnotModulo.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Forward.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PrintContext.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/EvarNormalize.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SpecializeAllWays.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Strings/StringMap.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/IsTrue.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/GeneralizeOverHoles.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructTrivial.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Notations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ProdForall.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DoWithHyp.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearDuplicates.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/Exists.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PrimeBound.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Mul.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Hints/Core.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/EvarExists.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ETransitivity.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RewriteHyp.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UniquePose.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearHead.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Zeta1.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SetEvars.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Beta1.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/Equality.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PullPush.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ESpecialize.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/WarnIfGoalsRemain.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/DefaultedTypes.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PrintGoal.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/UnfoldArg.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/DestructHyps.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/RevertUntil.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HeadConstrEq.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/FindHyp.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Delta1.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Head.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/ZSimplify.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SubstEvars.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Comparison.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Not.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/TransparentAssert.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearbodyAll.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearAll.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HasBody.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/EvarNormalize.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/NormalizeCommutativeIdentifier.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Logic/ImplAnd.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SideConditionsBeforeToAfter.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Delta1.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/PoseTermWithName.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearDuplicates.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearbodyAll.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ESpecialize.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ChangeInAll.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SubstEvars.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/OnSubterms.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/EvarExists.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ConstrFail.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SubstLet.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearFree.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SubstLet.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/SetEvars.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Contains.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/ClearAll.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/HasBody.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/GetGoal.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Revert.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/GlobalSettings.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/Test.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/ZUtil/Tactics/PullPush.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Bool/Equality.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Tactics/GetGoal.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Crypto/Util/Comparison.v

Uninstall ๐Ÿงน

Command
opam remove -y coq-fiat-crypto.0.0.16
Return code
0
Missing removes
none
Wrong removes
none