aboutsummaryrefslogtreecommitdiff
path: root/src/Util/SideConditions
Commit message (Expand)AuthorAge
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-11-01
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-10-23
* 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
* Add autosolve admit packageGravatar Jason Gross2017-11-12
* Use abstract in ring autosolveGravatar Jason Gross2017-11-12
* 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
* 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 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