index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
add sigma type proof irrelevance wisdom from ssreflect
Andres Erbsen
2016-06-25
*
folkwisdom: remove redundant idtac
Andres Erbsen
2016-06-24
*
incorporate `Program Definition` match statement handling advice from @mattam82
Andres Erbsen
2016-06-24
*
first draft of a "folk wisdom" document
Andres Erbsen
2016-06-24
*
nsatz_contradict can now handle invalid _ <> _ hypotheses
Jason Gross
2016-06-23
*
Update _CoqProject
Jason Gross
2016-06-23
*
Add Unit.v
Jason Gross
2016-06-23
*
Add equality on sum types
Jason Gross
2016-06-23
*
Merge pull request #8 from mit-plv/rsloan-pipeline-example-init
Jason Gross
2016-06-23
|
\
|
*
Remove examples for 8.4 compatibility
Robert Sloan
2016-06-23
|
*
Remove vestigal BoundedWord machinery
Robert Sloan
2016-06-23
*
|
Improve some tactics and lemmas
Jason Gross
2016-06-23
*
|
[break_match] should not be local
Jason Gross
2016-06-23
|
*
Remove vestigal GaloisField machinery
Robert Sloan
2016-06-23
*
|
Add tactics to Tactics, at most 2 sq-roots to Algebra
Jason Gross
2016-06-23
|
*
Update _CoqProject
Robert Sloan
2016-06-23
|
*
Make Pipeline.v Build on 8.4
Robert Sloan
2016-06-23
|
/
*
Merge pull request #7 from mit-plv/rsloan-unstable
Rob Sloan
2016-06-23
|
\
|
*
Remove unstable Pipeline.v examples from _CoqProject
Robert Sloan
2016-06-23
|
*
Add Language.v, Conversion.v to _CoqProject
Robert Sloan
2016-06-23
*
|
surjective homomorphism from group makes a group
Andres Erbsen
2016-06-23
|
*
Merge branch 'master' of github.com:mit-plv/fiat-crypto into public/rsloan-un...
Robert Sloan
2016-06-23
|
|
\
|
|
/
|
/
|
|
*
QhasmUtil.v: Remove 8.4-incompatible intro name
Robert Sloan
2016-06-23
|
*
Pipeline: several new examples
Robert Sloan
2016-06-23
*
|
Make [nsatz_contradict] better at inequalities
Jason Gross
2016-06-23
|
*
Pseudize Lemmas for Dual Operations
Robert Sloan
2016-06-23
*
|
[field_algebra] now knows that 0 <> -0 is false
Jason Gross
2016-06-23
*
|
Work around bug #4851 in nsatz
Jason Gross
2016-06-23
*
|
Add tactics for canonicalizing field (in)equalities
Jason Gross
2016-06-23
*
|
Rename the nonzero lemma to an iff lemma
Jason Gross
2016-06-23
*
|
Add mul_nonzero_nonzero_and to Algebra.v
Jason Gross
2016-06-23
|
*
Integrate Pseudize into Pipeline.v
Robert Sloan
2016-06-23
|
*
Integrate Pseudize into Pipeline.v
Robert Sloan
2016-06-23
|
*
Integrate Pseudize into Pipeline.v
Robert Sloan
2016-06-23
|
*
Pseudize Let_In with minor notations
Robert Sloan
2016-06-23
|
*
Pseudize Let_In
Robert Sloan
2016-06-23
|
*
Add Pseudize, Vectorize, Wordize to the build process
Robert Sloan
2016-06-22
|
*
Make Assembly modules 8.5-compatible
Robert Sloan
2016-06-22
|
*
Merge with public master
Robert Sloan
2016-06-22
|
|
\
|
|
/
|
/
|
*
|
EdDSA.Notations: indentation
Andres Erbsen
2016-06-22
*
|
Fix broken notations (hopefully)
Jason Gross
2016-06-22
*
|
Fix missing notations
Jason Gross
2016-06-22
*
|
Aggregate all level specifications not in Spec/*
Jason Gross
2016-06-22
*
|
Fix for broken abstract
Jason Gross
2016-06-22
|
*
Replace NPeano -> Nat in src/Spec/EdDSA
Robert Sloan
2016-06-22
*
|
Update _CoqProject
Jason Gross
2016-06-22
*
|
Add decidability util file
Jason Gross
2016-06-22
*
|
Flip the sense of the conditional in the makefile
Jason Gross
2016-06-22
*
|
Make Coq 8.5 the default target for Fiat-Crypto
Jason Gross
2016-06-22
*
|
Handle renaming of NPeano.pow to Nat.pow (#3)
Jason Gross
2016-06-22
[next]