aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/Ring_theory.v
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* | Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).Gravatar Hugo Herbelin2018-02-20
|/
* [stdlib] Fix warnings on deprecated `Add Setoid`Gravatar Emilio Jesus Gallego Arias2017-10-15
* [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Ring_theory: avoid overriding a few notationsGravatar Pierre Letouzey2016-09-28
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)Gravatar letouzey2010-10-14
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 06:06:21 +0000