index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
SideConditions
Commit message (
Collapse
)
Author
Age
*
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Hugo Herbelin
2018-11-01
|
|
|
|
Follow-up of acc4c460.
*
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Hugo Herbelin
2018-10-23
|
*
Add support for custom intro tactic in ring pkg, for speed
Jason Gross
2017-11-17
|
*
Add fast path for vm_decide (_ = false)
Jason Gross
2017-11-17
|
*
Add fast path for vm_decide (_ = true) package
Jason Gross
2017-11-17
|
*
Add native_compute evar packages
Jason Gross
2017-11-16
|
*
Add vm_compute_cbv_evar_package
Jason Gross
2017-11-16
|
*
Add ModInv autosolver
Jason Gross
2017-11-16
|
*
Add autosolve admit package
Jason Gross
2017-11-12
|
*
Use abstract in ring autosolve
Jason Gross
2017-11-12
|
*
First intro and split in Zring_prod_eq_tac, before cbv -
Jason Gross
2017-11-11
|
*
More modularity in autosolve
Jason Gross
2017-11-10
|
*
Separate case for handling option matches in autosolve
Jason Gross
2017-11-10
|
*
Add cbn [val] in autosolve
Jason Gross
2017-11-10
|
*
Base evard_package on evar_rel_package
Jason Gross
2017-11-07
|
*
Better way (hopefully) of projecting relation from evar package
Jason Gross
2017-11-07
|
*
Add notation for optional_evar_rel_package
Jason Gross
2017-11-07
|
*
Add support for autosolve packages with options
Jason Gross
2017-11-07
|
|
|
|
|
|
Following a suggestion from Adam to give default values for the options, which I do here by pushing the convoy pattern very deep into the structure of the automation, and hiding it there.
*
Allow pre-unfolding of autosolve things
Jason Gross
2017-11-07
|
*
Factor packages through evar_Prop_package, raw_evar_package
Jason Gross
2017-11-07
|
*
Remove function evar package in favor of generic rel one
Jason Gross
2017-11-07
|
*
Add evar_function_package
Jason Gross
2017-11-07
|
*
A bit more reorganization of autosolve
Jason Gross
2017-11-07
|
|
|
|
This lets other files import evar_package without having to be rebuilt every time a new package alias is added to Autosolve
*
Move SideConditionFramework
Jason Gross
2017-11-07