aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* Fix reductionGravatar Jason Gross2019-03-04
* Fix an issue with a proof from the previous commitGravatar Jason Gross2019-03-04
* Add some things to GENERATED rewriter fileGravatar Jason Gross2019-03-04
* Allow reifying cast and literalsGravatar Jason Gross2019-03-04
* Add some minor reflect thingsGravatar Jason Gross2019-03-04
* Add back build status indicator to README.mdGravatar Jason Gross2019-03-04
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Update a proof to work with previous commitGravatar Jason Gross2019-02-27
* Add UnderLets.mapGravatar Jason Gross2019-02-27
* finish porting barrett and montgomery code to new glue styleGravatar jadep2019-02-21
* 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
* Rename p484_64.c to p434_64.c (fix typo)Gravatar Daniel Hirche2019-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
* Improve travis stagesGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 04:10:40 +0000