aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* 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
* Base evard_package on evar_rel_packageGravatar Jason Gross2017-11-07
* Better way (hopefully) of projecting relation from evar packageGravatar Jason Gross2017-11-07
* Add notation for optional_evar_rel_packageGravatar Jason Gross2017-11-07
* Add HeadUnderBindersGravatar Jason Gross2017-11-07
* Add support for autosolve packages with optionsGravatar Jason Gross2017-11-07
* Allow pre-unfolding of autosolve thingsGravatar Jason Gross2017-11-07
* Factor packages through evar_Prop_package, raw_evar_packageGravatar Jason Gross2017-11-07
* Remove function evar package in favor of generic rel oneGravatar Jason Gross2017-11-07
* Add evar_function_packageGravatar Jason Gross2017-11-07
* A bit more reorganization of autosolveGravatar Jason Gross2017-11-07
* Move SideConditionFrameworkGravatar Jason Gross2017-11-07
* Deduplicate some codeGravatar Jason Gross2017-11-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 15:38:27 +0000