aboutsummaryrefslogtreecommitdiff
path: root/src/Util/SideConditions/ReductionPackages.v
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 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
* More modularity in autosolveGravatar Jason Gross2017-11-10