aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Update ladderstep displayGravatar Jason Gross2017-04-13
* Rewrite the ladderstep goalGravatar Jason Gross2017-04-13
* Handle implications in pipeline glueGravatar Jason Gross2017-04-13
* Add Util.Logic.ImplAndGravatar Jason Gross2017-04-13
* Add eexists_sig_etransitivity_for_rewrite_fun_RGravatar Jason Gross2017-04-13
* Add lift4_sig_sigGravatar Jason Gross2017-04-13
* Add eexists_sig_etransitivity_RGravatar Jason Gross2017-04-13
* Revert "update coq-scripts"Gravatar Jason Gross2017-04-13
* add CVE-2017-3732 to crypto-defects.mdGravatar Andres Erbsen2017-04-12
* update coq-scriptsGravatar Andres Erbsen2017-04-12
* Add commented out proof of equivalence in MxDHGravatar Jason Gross2017-04-12
* Add denoter for symbolic_exprGravatar Jason Gross2017-04-12
* SOp needs to hold the type of the arguments, for denoteGravatar Jason Gross2017-04-12
* Hold types in SFst and SSndGravatar Jason Gross2017-04-12
* More comment on Saturated.v, explaining representation and the [compact] oper...Gravatar jadep2017-04-11
* More WIP on CSE interpGravatar Jason Gross2017-04-11
* Extend cse context when inliningGravatar Jason Gross2017-04-11
* Add initial version of CSE interpGravatar Jason Gross2017-04-11
* Generalize prepend_prefixGravatar Jason Gross2017-04-10
* Fix missing 'by tac' in rewrite_hypGravatar Jason Gross2017-04-10
* Finish CSE_WfGravatar Jason Gross2017-04-10
* Finish most of wf for CSEGravatar Jason Gross2017-04-10
* Reorder parameters for ease of partial instantiation, add symbolic_expr_decGravatar Jason Gross2017-04-10
* Add dec_of_bool_decGravatar Jason Gross2017-04-10
* Add lookupb_extendb_fullGravatar Jason Gross2017-04-10
* Fix CSE to correctly symbolize expressionsGravatar Jason Gross2017-04-10
* Relax extendb, and prove a property about lengthGravatar Jason Gross2017-04-10
* Key on flat_type not base_type, in CSEGravatar Jason Gross2017-04-10
* Add flatten_binding_list_SmartVarfMap2_pair_In_splitGravatar Jason Gross2017-04-10
* Add flatten_binding_list_SmartVarfMap2_pair_same_in_eq2Gravatar Jason Gross2017-04-10
* Use Named.Context in CSE, so we can reuse context lemmasGravatar Jason Gross2017-04-10
* Add AListContext, WeakListContextGravatar Jason Gross2017-04-10
* Split off Compilers.Named.ContextGravatar Jason Gross2017-04-10
* Add rewrite_hyp ... by tacGravatar Jason Gross2017-04-10
* Finish the last of the admits in word-size-selection!Gravatar Jason Gross2017-04-09
* Split off ZUtil.Stabilization, finish IsBoundedBy!Gravatar Jason Gross2017-04-09
* Add Z.lt_le_flip_Proper_flip_implGravatar Jason Gross2017-04-09
* More wip on boundsGravatar Jason Gross2017-04-09
* Add Z.pow_nonneg to zarithGravatar Jason Gross2017-04-09
* More progress on boundsGravatar Jason Gross2017-04-09
* Don't take abs in upper_lor_and_boundsGravatar Jason Gross2017-04-09
* Make replace_with_neg more powerfulGravatar Jason Gross2017-04-09
* Handle more things in Z.peel_leGravatar Jason Gross2017-04-09
* Take more abs in Bounds.InterpretationGravatar Jason Gross2017-04-09
* Add Z.peel_leGravatar Jason Gross2017-04-09
* Factor out Z.{lor,land} proofs a bit moreGravatar Jason Gross2017-04-09
* Add Z.log2_up_le_mono to zarithGravatar Jason Gross2017-04-09
* Add Z.max_le_compat Z.min_le_compat to zarithGravatar Jason Gross2017-04-09
* Finish shift cases, extract out land, lor factsGravatar Jason Gross2017-04-09
* Add lemmas about shift bounds to ZUtilGravatar Jason Gross2017-04-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-04 16:51:15 +0000