aboutsummaryrefslogtreecommitdiff
BranchCommit messageAuthorAge
masterClean up notations after bbv removalBenjamin Barenblat2 years
 
 
AgeCommit messageAuthor
2019-04-26Clean up notations after bbv removalHEADmasterBenjamin Barenblat
2019-04-26Remove bbv dependencyBenjamin Barenblat
2019-04-26Remove WordUtilBenjamin Barenblat
2019-04-26Remove BoundedWordBenjamin Barenblat
2019-04-26Remove EdDSABenjamin Barenblat
2019-04-24Do less reduction in GENERATEDIdentifiersWithoutTypesJason Gross
2019-04-22Add some move/transport eq lemmasJason Gross
2019-04-22Add push_rew_fun_depJason Gross
2019-04-18Add Primitive.reflect_eq_prodJason Gross
2019-04-12Fix around coq/coq#262Jason Gross
2019-04-12Replace the python script with Ltac codeJason Gross
2019-04-11Don't include extraction .vo files in the all targetJason Gross
2019-04-11sed s'/RewriterProofs/RewriterAll/g'Jason Gross
2019-04-11rm src/*.out, now that we no longer generate theseJason Gross
2019-04-11Update README.md with new structure of the rewriterJason Gross
2019-04-11Make a single tactic to build the rewriterJason Gross
[...]
 
Clone
https://git.benjamin.barenblat.name/fiat-crypto.git
https://github.com/bbarenblat/fiat-crypto.git