aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Expand)AuthorAge
* Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
* Decimal: simple representation of base-10 numbersGravatar Pierre Letouzey2018-02-20
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Merge PR #845: Add Z.mod_div lemma to standard library.Gravatar Maxime Dénès2017-07-26
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Fix Zmod_div.Gravatar Russell O'Connor2017-06-29
| * Use forall for consistencyGravatar roconnor-blockstream2017-06-29
| * Add Z.mod_div lemma to standard library.Gravatar Russell O'Connor2017-06-29
|/
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Gravatar Hugo Herbelin2017-03-03
* Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Gravatar Hugo Herbelin2017-03-03
* Completing "few lemmas about Zneg" with lemmas also about Zpos.Gravatar Hugo Herbelin2017-03-03
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * Int.v: simplify Jason's commit 5b4e3aceGravatar Pierre Letouzey2016-05-04
| * Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Gravatar Pierre Letouzey2016-05-04
| |\
* | | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
|/ /
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Move compatibility notations to their proper filesGravatar Jason Gross2015-12-29
|/
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* eta contractionsGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toGravatar Hugo Herbelin2014-08-18
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Restore Zsqrt compat now that refine works fine with match.Gravatar aspiwack2013-11-02
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* More dynamic argument scopesGravatar letouzey2013-07-17
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
* Updating headers.Gravatar herbelin2012-08-08
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30