index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
_CoqProject
Commit message (
Expand
)
Author
Age
*
Add Algebra.SubsetoidRing
Jason Gross
2018-03-12
*
make update-_CoqProject
Jason Gross
2018-03-10
*
Prove another Barrett reduction variant.
David Benjamin
2018-03-09
*
Add new modular addition operation on Z
Jade Philipoom
2018-02-23
*
Add pointed types
Jason Gross
2018-02-18
*
Add a file to parse taps with Coq notations
Jason Gross
2018-02-14
*
Add some string utility functions
Jason Gross
2018-02-13
*
Add string conversions
Jason Gross
2018-02-11
*
Split off ZRange lemmas
Jason Gross
2018-02-10
*
Add some ZRange operations
Jason Gross
2018-02-10
*
minor updates needed to make it compile with bbv
Samuel Gruetter
2018-02-05
*
add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock di...
Samuel Gruetter
2018-02-05
*
Add x25519 donna versions with the new way of generating C code
Jason Gross
2018-01-15
*
Generate fecarry for solinas
Jason Gross
2018-01-10
*
Factor out fsatz lemmas
Jason Gross
2018-01-09
*
@davidben merged Jacobian+affine into Jacobian+Jacobian
Andres Erbsen
2018-01-09
*
Jacobian coordinates
Andres Erbsen
2018-01-09
*
Add Tactics.RunTacticAsConstr
Jason Gross
2017-11-26
*
Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v
Jason Gross
2017-11-24
*
Make a copy of Demo.v
Jason Gross
2017-11-24
*
Add ModInv autosolver
Jason Gross
2017-11-16
*
Update GeneralizeVar to ensure Wf
Jason Gross
2017-11-13
*
Make pipeline options more easily extensible
Jason Gross
2017-11-13
*
Add faster version of intros [a b] for reflective stuff
Jason Gross
2017-11-13
*
Add autosolve admit package
Jason Gross
2017-11-12
*
automatic modifications to _Coqproject with new files
jadep
2017-11-12
*
Add Decidable2Bool
Jason Gross
2017-11-11
*
Add ListUtil.Forall
Jason Gross
2017-11-11
*
More modularity in autosolve
Jason Gross
2017-11-10
*
Add HeadUnderBinders
Jason Gross
2017-11-07
*
A bit more reorganization of autosolve
Jason Gross
2017-11-07
*
Move SideConditionFramework
Jason Gross
2017-11-07
*
Add SideConditionFramework
Jason Gross
2017-11-07
*
Add type of bounded Z
Jason Gross
2017-11-02
*
make update-_CoqProject
Jason Gross
2017-11-02
*
Add MapBaseType
Jason Gross
2017-10-31
*
Add unextend_op
Jason Gross
2017-10-31
*
make update-_CoqProject
Jason Gross
2017-10-29
*
Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit
Jason Gross
2017-10-24
*
Add MapBaseType
Jason Gross
2017-10-23
*
Add InlineConstAndOpByRewrite
Jason Gross
2017-10-23
*
Add ZExtended/InlineConstAndOp.v
Jason Gross
2017-10-22
*
Add StripExpr
Jason Gross
2017-10-22
*
Add tight and loose bounds, no carry in add, sub
Jason Gross
2017-10-22
*
Add MapType
Jason Gross
2017-10-21
*
Add ZExtended/Syntax.v
Jason Gross
2017-10-20
*
Add GeneralizeVar{Wf,Interp}.v
Jason Gross
2017-10-20
*
Add GeneralizeVar
Jason Gross
2017-10-20
*
Add a version of exprf that lives in Set
Jason Gross
2017-10-20
*
Add Z.InlineConstAndOp*
Jason Gross
2017-10-20
[next]