index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
/
Logic.v
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Use the rew dependent notation in ex, ex2 proofs
Jason Gross
2017-05-28
*
Make theorems about ex equality Qed
Jason Gross
2017-05-28
*
Make new proofs of equality Qed
Jason Gross
2017-05-28
*
Use extended notation for ex, ex2 types
Jason Gross
2017-05-28
*
Replace [ex'] with [ex]
Jason Gross
2017-05-28
*
Use [rew_] instead of [eq_rect_] prefix
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 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
*
Functional choice <-> [inhabited] and [forall] commute
Gaetan Gilbert
2017-04-30
*
Small typo in comment
Vadim Zaliva
2017-04-26
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
*
\
Merge PR#442: Allow interactive editing of Coq.Init.Logic
Maxime Dénès
2017-03-17
|
\
\
*
|
|
Compatibility of iff wrt not and imp.
Hugo Herbelin
2017-03-03
|
|
*
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
|
/
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Remove Print Universe directive.
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Update headers.
Maxime Dénès
2015-01-12
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
*
Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".
Hugo Herbelin
2014-11-02
*
Basic lemmas about the algebraic structure of equality.
Hugo Herbelin
2014-05-31
*
Removing comment outdated since eta holds in conversion rule (this
Hugo Herbelin
2014-05-07
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Side effect free implementation of admit (Isabelle's oracle)
gareuselesinge
2013-08-08
*
Improving printing of 'rew' notation
herbelin
2013-05-05
*
Added group properties of eq_refl, eq_sym, eq_trans
herbelin
2013-04-17
*
Some lemmas on property of rewriting. It will probably be worth at
herbelin
2012-11-15
*
Removed a few calls to "Opaque" in Logic.v ineffective since at least
herbelin
2012-10-24
*
Updating headers.
herbelin
2012-08-08
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
Fixing a few bugs (see #2571) related to interpretation of multiple binders
herbelin
2012-04-06
*
No more use of tauto in Init/
pboutill
2012-01-19
*
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
*
Take benefit of bullets available by default in Prelude
herbelin
2011-08-10
*
Less ambitious application of a notation for eq_rect. We proposed
herbelin
2011-08-10
*
New proposition "rewrite Heq in H" for eq_rect (assuming that there is
herbelin
2011-08-08
*
All the parameters of or can be implicits.
pboutill
2011-07-26
*
Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)
herbelin
2011-07-16
*
Added a characterization of unique existence.
herbelin
2011-07-16
*
Used multiple lists of implicit arguments to transfer the choices of
herbelin
2010-10-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
[next]