aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* 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
* First intro and split in Zring_prod_eq_tac, before cbv -Gravatar Jason Gross2017-11-11
* More modularity in autosolveGravatar Jason Gross2017-11-10
* Separate case for handling option matches in autosolveGravatar Jason Gross2017-11-10
* Add cbn [val] in autosolveGravatar Jason Gross2017-11-10
* Fix opacity of dec_Forall, dec_ExistsGravatar Jason Gross2017-11-10
* Add dec_if_boolGravatar Jason Gross2017-11-10
* Generalize Tuple.dec_fieldwiseGravatar Jason Gross2017-11-09
* Generalize Forall2_forall_iffGravatar Jason Gross2017-11-09
* More generalization of fieldwise'_Proper to dependent typesGravatar Jason Gross2017-11-09
* Generalize fieldwise Proper lemmasGravatar Jason Gross2017-11-09
* Add fieldwise_lift_andGravatar Jason Gross2017-11-09
* Add more versions of fieldwise_ProperGravatar Jason Gross2017-11-09
* Add fieldwise_ProperGravatar Jason Gross2017-11-09
* Add fieldwise_eq_iffGravatar Jason Gross2017-11-09
* Add dec_Forall, dec_ExistsGravatar Jason Gross2017-11-09
* Add fieldwise_map_from_list_iffGravatar Jason Gross2017-11-09
* Add option_map_mapGravatar Jason Gross2017-11-07
* Add Tuple.dec_eq{,'}Gravatar Jason Gross2017-11-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 08:27:02 +0000