aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/InitialRing.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [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
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defGravatar letouzey2011-06-28
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Setoid_ring: some cleanups related with BinPos and BinNatGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* 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
* Euclidean division for NArithGravatar letouzey2010-02-10
* 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