fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
*	Various nsatz and field tactic improvements	Jason Gross	2016-06-24
*	Add a version of common_denominator w/o oversimpl	Jason Gross	2016-06-24
*	Remove a useless intro	Jason Gross	2016-06-24
*	ExtendedCoordinates: group.	Andres Erbsen	2016-06-24
*	isomorphism_to_subgroup_group	Andres Erbsen	2016-06-24
*	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
*	nsatz_contradict can now handle invalid _ <> _ hypotheses	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
\| *	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
\|\
\| *	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
* \|	Add decidability util file	Jason Gross	2016-06-22
* \|	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
\| *	Merge with plv/master	Robert Sloan	2016-06-22
\| \|\ \| \|/ \|/\|
\| *	Merging Pipeline.v	Robert Sloan	2016-06-22
\| \|\
\| * \	squash commits + revert makefile	Robert Sloan	2016-06-22
\| \|\ \