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
...
|
*
Use [rew_] instead of [eq_rect_] prefix
Jason Gross
2017-05-28
|
*
Add equality lemmas for sig2 and sigT2
Jason Gross
2017-05-28
|
*
Add lemmas for ex2
Jason Gross
2017-05-28
|
*
Use [rew] notations rather than [eq_rect]
Jason Gross
2017-05-28
|
*
Add an [inversion_sigma] tactic
Jason Gross
2017-05-28
|
*
Add lemmas about equality of sigma types
Jason Gross
2017-05-28
|
*
Use [rew_] instead of [eq_rect_] prefix
Jason Gross
2017-05-28
|
*
Use [rew] notations rather than [eq_rect]
Jason Gross
2017-05-28
|
*
Add more groupoid-like theorems about [eq]
Jason Gross
2017-05-28
|
/
*
Stop using auto with * in two proofs.
Théo Zimmermann
2017-05-16
*
Merge PR#201: Transparent abstract
Maxime Dénès
2017-05-11
|
\
*
\
Merge PR#605: Report a useful error for dependent induction
Maxime Dénès
2017-05-05
|
\
\
*
\
\
Merge PR#593: Functional choice <-> [inhabited] and [forall] commute
Maxime Dénès
2017-05-05
|
\
\
\
*
\
\
\
Merge PR#588: Allow interactive editing of {C,}Morphisms in PG
Maxime Dénès
2017-05-03
|
\
\
\
\
*
\
\
\
\
Merge PR#386: Better editing of the standard library in coqtop/PG
Maxime Dénès
2017-05-03
|
\
\
\
\
\
|
|
|
|
*
|
Report a useful error for dependent induction
Tej Chajed
2017-05-03
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
Reorganize comment documentation of ChoiceFacts.v
Gaetan Gilbert
2017-05-03
|
|
|
*
|
Functional choice <-> [inhabited] and [forall] commute
Gaetan Gilbert
2017-04-30
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Suppress warning message in stdlib.
Guillaume Melquiond
2017-04-29
|
|
*
|
Allow interactive editing of {C,}Morphisms in PG
Jason Gross
2017-04-28
|
|
/
/
|
/
|
|
|
*
|
Add .dir-locals.el and _CoqProject files for emacs stdlib editing
Jason Gross
2017-04-28
|
/
/
*
|
Merge PR#414: Some more theory on powerRZ.
Maxime Dénès
2017-04-27
|
\
\
*
\
\
Merge PR#584: Give andb_prop a simpler proof
Maxime Dénès
2017-04-27
|
\
\
\
*
|
|
|
Small typo in comment
Vadim Zaliva
2017-04-26
|
|
|
*
Add transparent_abstract tactic
Jason Gross
2017-04-25
|
|
_
|
/
|
/
|
|
|
*
|
Give andb_prop a simpler proof
Jason Gross
2017-04-25
|
/
/
*
|
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
|
|
_
|
_
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
[prev]
[next]
Jason Gross
Théo Zimmermann
Maxime Dénès
Tej Chajed
Gaetan Gilbert
Guillaume Melquiond
Vadim Zaliva
Jason Gross
Hugo Herbelin
George Stelle
Matej Kosik
Enrico Tassi