index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Merge PR#545: Add some hints to the "real" database to automatically discharg...
Maxime Dénès
2017-04-19
|
\
*
\
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
\
|
|
*
Add some hints to the "real" database to automatically discharge literal comp...
Guillaume Melquiond
2017-04-07
|
|
/
|
/
|
*
|
Merge PR#455: Farewell decl_mode
Maxime Dénès
2017-04-06
|
\
\
|
|
*
Merge branch 'origin/v8.5' into v8.6.
Hugo Herbelin
2017-04-06
|
|
|
\
*
|
|
|
Fix documentation typo (bug #5433).
Guillaume Melquiond
2017-04-02
*
|
|
|
Simplify some proofs.
Guillaume Melquiond
2017-04-02
*
|
|
|
Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.
Guillaume Melquiond
2017-03-30
*
|
|
|
Merge PR#469: Added take to VectorDef
Maxime Dénès
2017-03-30
|
\
\
\
\
|
*
|
|
|
Added take to VectorDef.
George Stelle
2017-03-30
*
|
|
|
|
Fixing missing PropFacts.v in Logic/vo.itarget.
Hugo Herbelin
2017-03-28
*
|
|
|
|
Merge PR#392: strengthened the statement of JMeq_eq_dep
Maxime Dénès
2017-03-24
|
\
\
\
\
\
*
\
\
\
\
\
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-23
|
\
\
\
\
\
\
|
|
|
_
|
_
|
/
/
|
|
/
|
|
|
|
*
|
|
|
|
|
Make IZR a morphism for field.
Guillaume Melquiond
2017-03-22
*
|
|
|
|
|
Change the parser and printer so that they use IZR for real constants.
Guillaume Melquiond
2017-03-22
*
|
|
|
|
|
Make IZR use a compact representation of integers.
Guillaume Melquiond
2017-03-22
*
|
|
|
|
|
Simplify some proofs using ring and field.
Guillaume Melquiond
2017-03-22
*
|
|
|
|
|
Add a forgotten (?) line to "theories/Logic/vo.itarget".
Matej Kosik
2017-03-19
*
|
|
|
|
|
Merge PR#442: Allow interactive editing of Coq.Init.Logic
Maxime Dénès
2017-03-17
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#451: Add η principles for sigma types
Maxime Dénès
2017-03-17
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto
Maxime Dénès
2017-03-14
|
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
Fix 3 unused-intro-pattern warnings in stdlib.
Théo Zimmermann
2017-03-14
*
|
|
|
|
|
|
|
Merge PR#318: Providing a file in the Logic library to work with extensional ...
Maxime Dénès
2017-03-09
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
Farewell decl_mode
Enrico Tassi
2017-03-07
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Merge PR#279: A few lemmas about iff and about orders on positive and Z
Maxime Dénès
2017-03-06
|
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
Strengthening some of the results in ChoiceFacts.v.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
Adding explicitly a file to work in the context of propositional extensionality.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
Adding a file providing extensional choice (i.e. choice over setoids).
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
Adding various properties and characterization of the extensional
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
Slightly unifying renaming in ChoiceFacts.v.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
Logic library: Adding a characterization of excluded-middle in term of
Hugo Herbelin
2017-03-03
*
|
|
|
|
|
|
|
|
Merge PR#273: Tidy stdlib
Maxime Dénès
2017-03-03
|
\
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
|
Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
|
Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
|
Completing "few lemmas about Zneg" with lemmas also about Zpos.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
|
A couple of other useful properties about compare_cont.
Hugo Herbelin
2017-03-03
|
|
*
|
|
|
|
|
|
|
Compatibility of iff wrt not and imp.
Hugo Herbelin
2017-03-03
|
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
Formatting references with surrounding brackets in Diaconescu.v.
Hugo Herbelin
2017-03-03
|
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Add η principles for sigma types
Jason Gross
2017-03-01
|
|
|
*
|
|
|
|
Remove some trailing whitespace in Init/Specif.v
Jason Gross
2017-03-01
|
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
Simplifying the proof of NoRetractToModalProposition.paradox in
Hugo Herbelin
2017-02-24
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Fixing a little bug in printing ex2 (type was printed "_" by default).
Hugo Herbelin
2017-02-23
|
|
*
|
|
|
Allow interactive editing of Coq.Init.Logic
Jason Gross
2017-02-21
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Ltac as a plugin.
Pierre-Marie Pédrot
2017-02-17
|
*
|
|
|
Proof clean-up.
Théo Zimmermann
2017-01-30
|
/
/
/
/
|
|
|
*
Fix some documentation typos.
Guillaume Melquiond
2016-12-26
*
|
|
|
Fix a typo in Hurkens.v comment
Jason Gross
2016-12-19
|
|
*
|
strengthened the statement of JMeq_eq_dep
Abhishek Anand
2016-12-11
|
|
/
/
|
/
|
|
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-30
|
\
|
|
|
*
|
Fix some documentation typos.
Guillaume Melquiond
2016-11-24
[next]
Maxime Dénès
Guillaume Melquiond
Hugo Herbelin
George Stelle
Matej Kosik
Théo Zimmermann
Enrico Tassi
Jason Gross
Pierre-Marie Pédrot
Jason Gross
Abhishek Anand