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 (
Expand
)
Author
Age
*
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Hugo Herbelin
2018-11-01
*
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
*
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
*
Move SideConditionFramework
Jason Gross
2017-11-07