Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add pow_ceil_mul_nat_divide_nonzero | 2017-12-15 | |
| | |||
* | Add reserved notation for infix @ for application | 2017-12-15 | |
| | |||
* | Add fast-path versions of [destruct_head] for unit,bool,True | 2017-12-12 | |
| | |||
* | Rename run_tactic_as_bool to is_success_run_tactic | 2017-11-26 | |
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144 | ||
* | Reserve a printing-only notation for function application | 2017-11-26 | |
| | | | | This sets the level and associativity in a common place, and will be useful for PHOAS application nodes | ||
* | Add Tactics.RunTacticAsConstr | 2017-11-26 | |
| | |||
* | Add reserved expr_let notation | 2017-11-26 | |
| | |||
* | Add support for custom intro tactic in ring pkg, for speed | 2017-11-17 | |
| | |||
* | Add fast path for vm_decide (_ = false) | 2017-11-17 | |
| | |||
* | Add fast path for vm_decide (_ = true) package | 2017-11-17 | |
| | |||
* | Add native_compute evar packages | 2017-11-16 | |
| | |||
* | Add vm_compute_cbv_evar_package | 2017-11-16 | |
| | |||
* | Add ModInv autosolver | 2017-11-16 | |
| | |||
* | Make pipeline options more easily extensible | 2017-11-13 | |
| | | | | | Also add a dummy option about renaming binders, to be used in an upcoming commit. | ||
* | Add autosolve admit package | 2017-11-12 | |
| | |||
* | Use abstract in ring autosolve | 2017-11-12 | |
| | |||
* | Add Decidable2Bool | 2017-11-11 | |
| | |||
* | Add ListUtil.Forall | 2017-11-11 | |
| | |||
* | First intro and split in Zring_prod_eq_tac, before cbv - | 2017-11-11 | |
| | |||
* | More modularity in autosolve | 2017-11-10 | |
| | |||
* | Separate case for handling option matches in autosolve | 2017-11-10 | |
| | |||
* | Add cbn [val] in autosolve | 2017-11-10 | |
| | |||
* | Fix opacity of dec_Forall, dec_Exists | 2017-11-10 | |
| | |||
* | Add dec_if_bool | 2017-11-10 | |
| | |||
* | Generalize Tuple.dec_fieldwise | 2017-11-09 | |
| | |||
* | Generalize Forall2_forall_iff | 2017-11-09 | |
| | |||
* | More generalization of fieldwise'_Proper to dependent types | 2017-11-09 | |
| | |||
* | Generalize fieldwise Proper lemmas | 2017-11-09 | |
| | |||
* | Add fieldwise_lift_and | 2017-11-09 | |
| | |||
* | Add more versions of fieldwise_Proper | 2017-11-09 | |
| | |||
* | Add fieldwise_Proper | 2017-11-09 | |
| | |||
* | Add fieldwise_eq_iff | 2017-11-09 | |
| | |||
* | Add dec_Forall, dec_Exists | 2017-11-09 | |
| | |||
* | Add fieldwise_map_from_list_iff | 2017-11-09 | |
| | |||
* | Add option_map_map | 2017-11-07 | |
| | |||
* | Add Tuple.dec_eq{,'} | 2017-11-07 | |
| | |||
* | Base evard_package on evar_rel_package | 2017-11-07 | |
| | |||
* | Better way (hopefully) of projecting relation from evar package | 2017-11-07 | |
| | |||
* | Add notation for optional_evar_rel_package | 2017-11-07 | |
| | |||
* | Add HeadUnderBinders | 2017-11-07 | |
| | |||
* | Add support for autosolve packages with options | 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 | 2017-11-07 | |
| | |||
* | Factor packages through evar_Prop_package, raw_evar_package | 2017-11-07 | |
| | |||
* | Remove function evar package in favor of generic rel one | 2017-11-07 | |
| | |||
* | Add evar_function_package | 2017-11-07 | |
| | |||
* | A bit more reorganization of autosolve | 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 | 2017-11-07 | |
| | |||
* | Deduplicate some code | 2017-11-06 | |
| | |||
* | More id_with_alt_cps updates | 2017-11-06 | |
| | |||
* | Update versions of id_with_alt_cps | 2017-11-06 | |
| | | | | These type signatures allow better reification |