aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/Ring_polynom.v
Commit message (Expand)AuthorAge
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Better fix of e5c025Gravatar Pierre Boutillier2014-08-05
* Fix to make Coq compile, I think this should still be accepted.Gravatar Matthieu Sozeau2014-08-03
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing an incompleteness of the ring/field tacticsGravatar amahboub2013-08-23
* Ring_polynom : shorter proof for Psub_okGravatar letouzey2013-08-22
* Updating headers.Gravatar herbelin2012-08-08
* Ring_polynom : a restricted simpl instead of a unfold;foldGravatar letouzey2012-07-07
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
* More cleanup in Ring_polynom and EnvRingGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)Gravatar letouzey2010-10-14
* 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-11-30 12:40:59 +0000