aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* git submodule update --remote --recursiveGravatar Andres Erbsen2018-02-24
* coqprime in COQPATH (closes #269)Gravatar Andres Erbsen2018-02-24
* Add ZRange.intersectionGravatar Jason Gross2018-02-23
* Fix a typoGravatar Jason Gross2018-02-23
* Add some bounds operations to ZRangeGravatar Jason Gross2018-02-23
* Add ZRange.oppGravatar Jason Gross2018-02-23
* move things from ZUtil.v into Div.vGravatar Jade Philipoom2018-02-23
* add three proofs to ZUtilGravatar Jade Philipoom2018-02-23
* add two proofs about listsGravatar Jade Philipoom2018-02-23
* add proof about Z.equiv_moduloGravatar Jade Philipoom2018-02-23
* create rewrite database for saturated operations on ZGravatar Jade Philipoom2018-02-23
* Add new modular addition operation on ZGravatar Jade Philipoom2018-02-23
* NumTheoryUtil: make coqprime dependencies explicitGravatar Andres Erbsen2018-02-19
* Strip the pointed instance names off of the default value in list expansionGravatar Jason Gross2018-02-18
* Add expand_lists tacticGravatar Jason Gross2018-02-18
* Add pointed typesGravatar Jason Gross2018-02-18
* Fix a proof for Coq 8.7Gravatar Jason Gross2018-02-17
* Add lemmas about always_invert_Some and bindGravatar Jason Gross2018-02-17
* Add always_invert_SomeGravatar Jason Gross2018-02-17
* Add a file to parse taps with Coq notationsGravatar Jason Gross2018-02-14
* Add some string utility functionsGravatar Jason Gross2018-02-13
* Add expand_list_correct to ListUtilGravatar Jason Gross2018-02-12
* Add string conversionsGravatar Jason Gross2018-02-11
* Add notation for option_bindGravatar Jason Gross2018-02-10
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* Add some ZRange operationsGravatar Jason Gross2018-02-10
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* Add better levels / printing for bind notationsGravatar Jason Gross2018-01-16
* Add a comment for why Z.peano_rect_strong exists.Gravatar David Benjamin2018-01-14
* Factor out fsatz lemmasGravatar Jason Gross2018-01-09
* Add @@ infix notationGravatar Jason Gross2018-01-06
* Add some reserved notations for cps stuffGravatar Jason Gross2017-12-27
* Add pow_ceil_mul_nat_divide_nonzeroGravatar Jason Gross2017-12-15
* Add reserved notation for infix @ for applicationGravatar Jason Gross2017-12-15
* Add fast-path versions of [destruct_head] for unit,bool,TrueGravatar Jason Gross2017-12-12
* Rename run_tactic_as_bool to is_success_run_tacticGravatar Jason Gross2017-11-26
* Reserve a printing-only notation for function applicationGravatar Jason Gross2017-11-26
* Add Tactics.RunTacticAsConstrGravatar Jason Gross2017-11-26
* Add reserved expr_let notationGravatar Jason Gross2017-11-26
* Add support for custom intro tactic in ring pkg, for speedGravatar Jason Gross2017-11-17
* Add fast path for vm_decide (_ = false)Gravatar Jason Gross2017-11-17
* Add fast path for vm_decide (_ = true) packageGravatar Jason Gross2017-11-17
* Add native_compute evar packagesGravatar Jason Gross2017-11-16
* Add vm_compute_cbv_evar_packageGravatar Jason Gross2017-11-16
* Add ModInv autosolverGravatar Jason Gross2017-11-16
* Make pipeline options more easily extensibleGravatar Jason Gross2017-11-13
* Add autosolve admit packageGravatar Jason Gross2017-11-12
* Use abstract in ring autosolveGravatar Jason Gross2017-11-12
* Add Decidable2BoolGravatar Jason Gross2017-11-11
* Add ListUtil.ForallGravatar Jason Gross2017-11-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 01:53:03 +0000