aboutsummaryrefslogtreecommitdiff
BranchCommit messageAuthorAge
masterClean up notations after bbv removalGravatar Benjamin Barenblat5 years
 
 
AgeCommit messageAuthor
2019-04-26Clean up notations after bbv removalHEADmasterGravatar Benjamin Barenblat
2019-04-26Remove bbv dependencyGravatar Benjamin Barenblat
2019-04-26Remove WordUtilGravatar Benjamin Barenblat
2019-04-26Remove BoundedWordGravatar Benjamin Barenblat
2019-04-26Remove EdDSAGravatar Benjamin Barenblat
2019-04-24Do less reduction in GENERATEDIdentifiersWithoutTypesGravatar Jason Gross
2019-04-22Add some move/transport eq lemmasGravatar Jason Gross
2019-04-22Add push_rew_fun_depGravatar Jason Gross
2019-04-18Add Primitive.reflect_eq_prodGravatar Jason Gross
2019-04-12Fix around coq/coq#262Gravatar Jason Gross
2019-04-12Replace the python script with Ltac codeGravatar Jason Gross
2019-04-11Don't include extraction .vo files in the all targetGravatar Jason Gross
2019-04-11sed s'/RewriterProofs/RewriterAll/g'Gravatar Jason Gross
2019-04-11rm src/*.out, now that we no longer generate theseGravatar Jason Gross
2019-04-11Update README.md with new structure of the rewriterGravatar Jason Gross
2019-04-11Make a single tactic to build the rewriterGravatar Jason Gross
[...]
 
Clone
https://git.benjamin.barenblat.name/fiat-crypto.git
https://github.com/bbarenblat/fiat-crypto.git