aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Clean up notations after bbv removalHEADmasterBenjamin Barenblat2019-04-26
* Remove WordUtilBenjamin Barenblat2019-04-26
* Remove BoundedWordBenjamin Barenblat2019-04-26
* Remove EdDSABenjamin Barenblat2019-04-26
* Do less reduction in GENERATEDIdentifiersWithoutTypesJason Gross2019-04-24
* Add some move/transport eq lemmasJason Gross2019-04-22
* Add push_rew_fun_depJason Gross2019-04-22
* Add Primitive.reflect_eq_prodJason Gross2019-04-18
* Fix around coq/coq#262Jason Gross2019-04-12
* Replace the python script with Ltac codeJason Gross2019-04-12
* sed s'/RewriterProofs/RewriterAll/g'Jason Gross2019-04-11
* rm src/*.out, now that we no longer generate theseJason Gross2019-04-11
* Make a single tactic to build the rewriterJason Gross2019-04-11
* Automate more of the rewriter, and factor out rule-specific thingsJason Gross2019-04-11
* Add base.reflect_{base,type}_beq and type.reflect_type_beqJason Gross2019-04-10
* Fix for Coq 8.8Jason Gross2019-04-09
* Automate more of the rewriter reification, proofJason Gross2019-04-09
* Fix for 8.8Jason Gross2019-04-05
* Generalize correctly in strip_literal_casts_rewrite_rulesTJason Gross2019-04-05
* Add some bool eqb lemmasJason Gross2019-04-05
* Don't eagerly unfold boolean functions, hopefully, in tc reflect searchJason Gross2019-04-05
* Hint reflect on negbJason Gross2019-04-05
* Add interp_related lemmasJason Gross2019-04-05
* Add some more underlets lemmasJason Gross2019-04-04
* Add UnderLets flat_map interp proofs,other changesJason Gross2019-04-04
* partition -> Partition.partition to prevent confusion with List.partitionjadep2019-04-03
* fix typojadep2019-04-03
* remove unnecessary imports from Primitives.vjadep2019-04-03
* fix up imports in SmallExamples.vjadep2019-04-03
* update import statementsjadep2019-04-03
* rename some thingsjadep2019-04-03
* fix imports and qualifiers so everything buildsjadep2019-04-03
* remove extraneous module identifiersjadep2019-04-03
* update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...jadep2019-04-03
* split up Arithmetic (imports etc. not yet fixed, does not build)jadep2019-04-03
* Add Z.combine_at_bitwidthJason Gross2019-04-02
* Factor out rewriter rulesJason Gross2019-03-31
* Fix a non-terminated commentJason Gross2019-03-31
* Add some comments based on CR requestsJason Gross2019-03-31
* Fix issue with refolding in eapply in < 8.9Jason Gross2019-03-31
* Finish reifying list lemmasJason Gross2019-03-31
* Add constr_fail and constr_fail_withJason Gross2019-03-31
* improve zero_bounds tacticjadep2019-03-26
* add some hints to the global databasesjadep2019-03-26
* remove Derive to fix 8.7jadep2019-03-25
* fix montgomeryjadep2019-03-25
* remove 2: syntax so I don't break 8.7jadep2019-03-25
* fix up a messy proofjadep2019-03-25
* Move some lemmas to appropriate placesjadep2019-03-25
* finish proofsjadep2019-03-25