aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/Ring_theory.v
AgeCommit message (Expand)Author
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).Hugo Herbelin
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2010-10-14Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)letouzey
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:24:06 +0000