aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add 8.7-only CacheTermGravatar Jason Gross2017-10-18
* Add a Require Import FunInd (Function isn't loaded by default anymore)Gravatar Pierre Letouzey2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
* Allow instantiation of cps type arguments by unfoldingGravatar Jason Gross2017-10-17
* Add CacheTermGravatar Jason Gross2017-10-17
* Allow unfolding of mapi_with_cps to specialize the function to the type argum...Gravatar Jason Gross2017-10-17
* Work around bug #5341Gravatar Jason Gross2017-10-17
* Add strip_subst_localGravatar Jason Gross2017-10-15
* Add pow_ceil_mul_nat_divide_upperboundGravatar Jason Gross2017-10-13
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
* Add update_by_tac_if_not_existsGravatar Jason Gross2017-10-10
* TagList: make get error, and fix bugsGravatar Jason Gross2017-10-10
* Add TagListGravatar Jason Gross2017-10-10
* Add notationsGravatar Jason Gross2017-10-10
* Add pow_ceil_mul_nat_nonnegGravatar Jason Gross2017-10-05
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
* Add some ZUtil lemmasGravatar Jason Gross2017-10-03
* Add decidable equality with nilGravatar Jason Gross2017-08-13
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* More fine-grained importsGravatar Jason Gross2017-07-08
* Add UnfoldArgGravatar Jason Gross2017-07-08
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
* Add wrappers for subborrow and add_with_get_carry so they work when it is not...Gravatar jadep2017-06-29
* remove unused admit (has been moved to Tuple.v)Gravatar jadep2017-06-26
* Prove map2_appendGravatar Jason Gross2017-06-25
* write and prove Tuple.map2_cpsGravatar jadep2017-06-25
* Fix a typo in push_Zmod that was causing loopingGravatar Jason Gross2017-06-22
* Fix some minor naming bugs in sig_assoc tacticsGravatar Jason Gross2017-06-22
* src/Demo.v: a 200-line introduction to BaseSystem ideasGravatar Andres Erbsen2017-06-21
* Prove In_to_list_left_tl, In_left_hd, to_list_left_appendGravatar Jason Gross2017-06-21
* Add is_bounded_by_None_repeat_In_iff_ltGravatar Jason Gross2017-06-20
* Add fold_left_orb_true, fold_left_orb_pullGravatar Jason Gross2017-06-20
* Add is_bounded_by_None_repeat_In_iffGravatar Jason Gross2017-06-20
* [Require NatUtil] should not change [tauto]Gravatar Jason Gross2017-06-19
* Add ModInvGravatar Jason Gross2017-06-18
* Stronger zero_boundsGravatar Jason Gross2017-06-18
* Add div_nonneg to zarithGravatar Jason Gross2017-06-18
* Add Z.div_nonnegGravatar Jason Gross2017-06-18
* Add eq_ZToWordGravatar Jason Gross2017-06-17
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
* CPSify Saturated API in preparation for CPSifying Montgomery (see #194)Gravatar jadep2017-06-15
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
* Fix a changed case in the proof in loop.vGravatar Jason Gross2017-06-15
* Better for_loop induction principleGravatar Jason Gross2017-06-15
* Export ZUtil.Z2Nat in ZUtilGravatar Jason Gross2017-06-15
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 19:38:10 +0000