aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Simplify a proof that no longer needs more hintsGravatar Jason Gross2016-07-01
* Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01
* Add some proofs about Z.div and Z.mulGravatar Jason Gross2016-07-01
* Add [specialize_by] tacticGravatar Jason Gross2016-07-01
* Fix a typo in Zsplit_sumsGravatar Jason Gross2016-07-01
* Add tactic to split sums and differences in inequalitiesGravatar Jason Gross2016-07-01
* Add more caches to .gitignore (nra, csdp)Gravatar Jason Gross2016-07-01
* Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
* Update .gitignore with lia, nia cachesGravatar Jason Gross2016-07-01
* Add a proof of 2 * x - x = xGravatar Jason Gross2016-06-30
* Add a classification of n / m < 0Gravatar Jason Gross2016-06-30
* Add a tactic for making use of destructed <? in ZGravatar Jason Gross2016-06-30
* Prove that a ^ k <> 0Gravatar Jason Gross2016-06-30
* Add pow_Zpow to Util.ZUtilGravatar Jason Gross2016-06-30
* Simplify conservative_common_denominatorGravatar Jason Gross2016-06-29
* Don't generate goals [False] in conservative_common_denominator_allGravatar Jason Gross2016-06-29
* Fix [only_two_square_roots] to not loopGravatar Jason Gross2016-06-29
* Allow side-conditions in common denom. all in hypsGravatar Jason Gross2016-06-29
* Handle fractions in denominatorsGravatar Jason Gross2016-06-29
* Clear symmetric duplicates in clear_algebraic_duplicatesGravatar Jason Gross2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Update crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Create crypto-defects.mdGravatar Andres Erbsen2016-06-29
* Fix a typo in the previous commitGravatar Jason Gross2016-06-28
* [super_nstaz]: Handle side-conditions from [nsatz]Gravatar Jason Gross2016-06-28
* Revert "CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge"Gravatar Andres Erbsen2016-06-28
* No more anomalies from super_nsatz, hopefullyGravatar Jason Gross2016-06-28
* Fix field_algebra in 8.4Gravatar Jason Gross2016-06-28
* CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahngeGravatar Andres Erbsen2016-06-28
* Also install libcoq-ocamlGravatar Jason Gross2016-06-28
* Add many versions of Coq 8.4 to travisGravatar Jason Gross2016-06-28
* Fix a typo (missing .)Gravatar Jason Gross2016-06-28
* Fix super_nsatz tactic to be better about orderingGravatar Jason Gross2016-06-28
* EdDSARefinement: work around rewrite_strat for 8.4Gravatar Andres Erbsen2016-06-28
* Tuple: from_list_to_listGravatar Andres Erbsen2016-06-28
* Try a faster way of solving some inequalities resulting from common_denominatorGravatar Jason Gross2016-06-27
* Actual fix for super_nsatzGravatar Jason Gross2016-06-27
* Fix super_nstaz to not errorGravatar Jason Gross2016-06-27
* Add a super_nsatz tacticGravatar Jason Gross2016-06-27
* eddsa refinement setupGravatar Andres Erbsen2016-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 00:51:59 +0000