index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Classes
/
DecidableClass.v
Age
Commit message (
Expand
)
Author
2020-12-15
Modify Classes/DecidableClass.v to compile with -mangle-names
Jasper Hugunin
2020-11-04
[stdlib] Decidable instance for negation
Yishuai Li
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-10-11
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-10
Give the same argument name for the record binder of type class
Matthieu Sozeau
2014-07-09
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2012-08-08
Updating headers.
herbelin
2012-01-13
Added the decidability of (<=) on nat.
ppedrot
2012-01-06
Added a typeclass-based system to reason on decidable propositions.
ppedrot
