aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* adapt barrett to new glue codeGravatar jadep2019-02-21
* Make Qed not take foreverGravatar jadep2019-02-21
* start adapting Montgomery to new glue codeGravatar jadep2019-02-21
* Add base.{base_,}interp_beqGravatar Jason Gross2019-02-20
* Update .out filesGravatar Jason Gross2019-02-18
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
* fix cast admits in FancyGravatar jadep2019-02-15
* Fix missing "= true" in a tactic so [Admitted] is unneccesary.Gravatar jadep2019-02-15
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
* Insert casts before literals during bounds analysisGravatar Jason Gross2019-02-11
* clean up and factor out cast-admit so that [Print Assumptions] is more fine-g...Gravatar jadep2019-02-08
* cleanupGravatar jadep2019-02-08
* remove some TODOs -- actually, the final proof does not rely on the unused va...Gravatar jadep2019-02-08
* fix Montgomery proof and clean up a littleGravatar jadep2019-02-08
* remove 2: syntax so 8.7 buildsGravatar jadep2019-02-07
* Fix instruction-order admit; still neads cleanupGravatar jadep2019-02-07
* Use Preconditions: Postconditions:, rather than /\ and ->Gravatar Jason Gross2019-02-02
* More minor improvements in docstringsGravatar Jason Gross2019-02-02
* Rename docstring generator based on Andres' suggestionGravatar Jason Gross2019-02-02
* Update with davidben's and Andres' suggestionsGravatar Jason Gross2019-02-02
* Drop `map λ` bits in docstringsGravatar Jason Gross2019-02-02
* Address code review comments to improve docstringsGravatar Jason Gross2019-02-02
* Add autogenerated docstrings to synthesized codeGravatar Jason Gross2019-02-02
* Add zrange_rect{,_Proper,_Proper_dep}Gravatar Jason Gross2019-02-02
* Add option_beq_heteroGravatar Jason Gross2019-02-02
* Remove an unused argumentGravatar Jason Gross2019-02-01
* Uncps unify_extractedGravatar Jason Gross2019-02-01
* Reduce more in mulmod and squaremodGravatar Jason Gross2019-01-26
* Add an example to SlowPrimeSynthesisExamples.vGravatar Jason Gross2019-01-26
* Also display the carry chain in a commentGravatar Jason Gross2019-01-26
* Add better computation of carry chainGravatar Jason Gross2019-01-26
* Actually support Nat.eqb in reificationGravatar Jason Gross2019-01-25
* Support Nat.eqb in reificationGravatar Jason Gross2019-01-25
* Add remove_duplicatesGravatar Jason Gross2019-01-24
* Make trivial instances explicitGravatar Maxime Dénès2019-01-24
* Give slightly more standard usage stringsGravatar Jason Gross2019-01-23
* Mention the separator (spaces) of the list argGravatar Jason Gross2019-01-23
* Split up PushButtonSynthesis.vGravatar Jason Gross2019-01-18
* Define String.replaceGravatar Jason Gross2019-01-18
* Be stricter about rejecting command line argumentsGravatar Jason Gross2019-01-18
* Don't allow r[0~>0] ranges in fancy synthesisGravatar Jason Gross2019-01-17
* Remove ? notationGravatar Jason Gross2019-01-17
* Move print statements to Barrett and Montgomery filesGravatar jadep2019-01-17
* prune dependencies from Barrett256 and Montgomery256Gravatar jadep2019-01-17
* Prune dependencies of Prod.v and fix upGravatar jadep2019-01-17
* Rename Translation.vGravatar jadep2019-01-17
* Prune Translation.v deps and move tactics from other files [WIP]Gravatar jadep2019-01-17
* clean up and prune deps of Spec.vGravatar jadep2019-01-17
* Fix up MontgomeryGravatar jadep2019-01-17
* Make Montgomery take arguments separately instead of as a pairGravatar jadep2019-01-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 03:36:00 +0000