aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Add nonautogenerated-specific{,-display} targetsGravatar Jason Gross2017-10-23
* Add inline_const_and_op{f,} specializationsGravatar Jason Gross2017-10-22
* Add another unfolding databaseGravatar Jason Gross2017-10-22
* Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2Gravatar Jason Gross2017-10-22
* Add ZExtended/InlineConstAndOp.vGravatar Jason Gross2017-10-22
* Add StripExprGravatar Jason Gross2017-10-22
* Add tight and loose bounds, no carry in add, subGravatar Jason Gross2017-10-22
* Unfold P.bound1 in fenzGravatar Jason Gross2017-10-21
* Add MapTypeGravatar Jason Gross2017-10-21
* Add SmartValf_optionGravatar Jason Gross2017-10-20
* Add ZExtended/Syntax.vGravatar Jason Gross2017-10-20
* Add GeneralizeVar{Wf,Interp}.vGravatar Jason Gross2017-10-20
* Generalize wf_compile a bitGravatar Jason Gross2017-10-20
* Add GeneralizeVarGravatar Jason Gross2017-10-20
* Add a version of exprf that lives in SetGravatar Jason Gross2017-10-20
* Add Z.InlineConstAndOp*Gravatar Jason Gross2017-10-20
* Add InlineConstAndOpInterp.vGravatar Jason Gross2017-10-20
* Add interpf_invert_PairsConstGravatar Jason Gross2017-10-20
* Add InlineConstAndOpWf.vGravatar Jason Gross2017-10-20
* Add wff_SmartPairf_SmartVarfMap_sameGravatar Jason Gross2017-10-20
* Add SmartVarVarf_Pair, SmartPairfSmartVarVarf_SmartVarfGravatar Jason Gross2017-10-20
* Add wff_invert_PairsConstGravatar Jason Gross2017-10-20
* Better typing on postprocess_for_const_and_opGravatar Jason Gross2017-10-20
* Add InlineConstAndOpGravatar Jason Gross2017-10-20
* Add curry{3,4}Gravatar Jason Gross2017-10-20
* Fix arguments of previous commitGravatar Jason Gross2017-10-20
* Add invert_PairsConstGravatar Jason Gross2017-10-20
* Add invert_PairsGravatar Jason Gross2017-10-20
* Allow partial-inlining in the inlinerGravatar Jason Gross2017-10-20
* gmpvar.c: slightly faster montgomery ladder implementation using mpn_* functionsGravatar Andres Erbsen2017-10-20
* gmpsec.c: generic constant-time montgomery ladder implementation using mpn_se...Gravatar Andres Erbsen2017-10-20
* Allow inlining expressions not returning TbaseGravatar Jason Gross2017-10-20
* Prove flatten_binding_list_interpf_SmartPairf_sameGravatar Jason Gross2017-10-20
* Add wff_SmartPairfGravatar Jason Gross2017-10-20
* Fix bug in previous commitGravatar Jason Gross2017-10-20
* Use div_cps, modulo_cpsGravatar Jason Gross2017-10-20
* gmpsec: towards an mxladder implementationGravatar Andres Erbsen2017-10-19
* invscratch_szGravatar Andres Erbsen2017-10-19
* indentGravatar Andres Erbsen2017-10-19
* Use fold_right_cps2 to get eqb_cps to get the right continuation typeGravatar Jason Gross2017-10-19
* gmpsec.c: field arithmetic implementation using GMP mpn_sec_*Gravatar Andres Erbsen2017-10-19
* Add more unfolds to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-19
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* Add mul_split_cps'Gravatar Jason Gross2017-10-19
* Add FancyMachine256 to selected-specificGravatar Jason Gross2017-10-19
* Move tactics around in src/Arithmetic/CoreUnfolder.vGravatar Jason Gross2017-10-19
* Update ZUtil cps definitionsGravatar Jason Gross2017-10-19
* Pattern over cps lemmas in Arithmetic/CoreGravatar Jason Gross2017-10-19
* Add ZUtil.CPSGravatar Jason Gross2017-10-19
* Don't make autogenerated files in `coq`/default targetGravatar Jason Gross2017-10-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 04:31:56 +0000