index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
setoid_ring
/
Ring_polynom.v
Age
Commit message (
Expand
)
Author
2019-05-25
Documenting syntax "injection ... as [= pat1 ... patn ]".
Hugo Herbelin
2019-03-30
Error when [foo.(bar)] is used with nonprojection [bar]
Gaëtan Gilbert
2019-02-28
Implement a method for manual declaration of implicits.
Jasper Hugunin
2018-12-19
Put #[universes(template)] on all auto template spots in stdlib
Gaëtan Gilbert
2018-10-10
[coqlib] Rebindable Coqlib namespace.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-10-05
[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-06-18
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-10-01
Fix cbn behavior wrt simpl no match
Pierre Boutillier
2014-09-27
Keyed unification option, compiling the whole standard library
Matthieu Sozeau
2014-08-05
Better fix of e5c025
Pierre Boutillier
2014-08-03
Fix to make Coq compile, I think this should still be accepted.
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2013-08-23
Fixing an incompleteness of the ring/field tactics
amahboub
2013-08-22
Ring_polynom : shorter proof for Psub_ok
letouzey
2012-08-08
Updating headers.
herbelin
2012-07-07
Ring_polynom : a restricted simpl instead of a unfold;fold
letouzey
2012-07-05
rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite
letouzey
2012-07-05
More cleanup in Ring_polynom and EnvRing
letouzey
2012-07-05
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2011-05-05
Modularization of BinPos + fixes in Stdlib
letouzey
2010-10-14
Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)
letouzey
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-07-18
Reverted 13293 commited mistakenly. Sorry for the noise.
herbelin
2010-07-18
Tentative de suppression de l'import automatique des hints et coercions.
herbelin
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
