aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Factor out rewriter rulesGravatar Jason Gross2019-03-31
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Add better computation of carry chainGravatar Jason Gross2019-01-26
* Split up PushButtonSynthesis.vGravatar Jason Gross2019-01-18
* Rename Translation.vGravatar jadep2019-01-17
* separate toplevel2 into several files; fix up final barrett proofGravatar jadep2019-01-17
* Move StringMap into Strings/Gravatar Jason Gross2019-01-15
* Add StringMapGravatar Jason Gross2019-01-15
* Add String_as_OTGravatar Jason Gross2019-01-15
* Autocompute s and c in WBW MontgomeryGravatar Jason Gross2019-01-14
* remove old pipelineGravatar Andres Erbsen2019-01-09
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* new pipeline: refactor glue, split into more filesGravatar Jason Gross2019-01-05
* Add has_body tacticGravatar Jason Gross2018-12-21
* Finish rewriter proofs modulo funextGravatar Jason Gross2018-12-19
* Add ZRange.OperationBoundsGravatar Jason Gross2018-12-11
* Add related_sigT_by_eqGravatar Jason Gross2018-11-16
* Add PositiveSet FactsGravatar Jason Gross2018-10-29
* Add some lemmas about ex, and, eqGravatar Jason Gross2018-10-29
* Add CPSId tacticsGravatar Jason Gross2018-10-28
* Add some equality lemmas about Positive{Map,Set}Gravatar Jason Gross2018-10-23
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
* Add ListUtil.ForallInGravatar Jason Gross2018-10-09
* Add some lemmas about Bool.reflectGravatar Jason Gross2018-09-27
* Add list_elementwise_eqlistAGravatar Jason Gross2018-09-14
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Add a rudimentary arg parse moduleGravatar Jason Gross2018-08-30
* Add src/Util/PER.vGravatar Jason Gross2018-08-29
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Bump bbvGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Add more operation-specific proofsGravatar Jason Gross2018-08-21
* Add the file proving split_bounds correctGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
* Add related_iff_app_curriedGravatar Jason Gross2018-08-06
* Add GENERATEDIdentifiersWithoutTypesProofs.vGravatar Jason Gross2018-08-02
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* Add Wf proofs about MiscCompilerPassesGravatar Jason Gross2018-07-26
* Add Wf lemmas about SubstVarGravatar Jason Gross2018-07-26
* Add basic wf proofsGravatar Jason Gross2018-07-26
* Add some inversion lemmas and tacticsGravatar Jason Gross2018-07-25
* Montgomery reduction in new pipelineGravatar Jason Gross2018-07-21
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 03:43:52 +0000