index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Logic
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-08
|
\
|
*
Fixing unexpected "noise" introduced in commit 24d5448c.
Hugo Herbelin
2016-10-06
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
More tests for tactic "subst".
Hugo Herbelin
2016-10-02
*
|
extensionality: Handle dependently-used hypotheses
Jason Gross
2016-09-19
*
|
Adding an "extensionality in H" tactic which applies functional
Hugo Herbelin
2016-09-19
|
/
*
Typo in a comment of stdlib.
Hugo Herbelin
2016-07-08
*
Moving the Tauto tactic to proper Ltac.
Pierre-Marie Pédrot
2016-02-22
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
*
Fix bug #4503: mixing universe polymorphic and monomorphic
Matthieu Sozeau
2016-01-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
|
|
*
Refine tactic now shelves unifiable holes.
Pierre-Marie Pédrot
2015-12-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
|
Fix to previous commit (ClassicalFacts.v).
Hugo Herbelin
2015-12-05
*
|
Adding proofs on the relation between excluded-middle and minimization.
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
*
|
Adding an amazing property of Prop.
Hugo Herbelin
2015-11-07
|
/
*
Minor modifications to WeakFanTheorem.
Hugo Herbelin
2015-09-08
*
Remove some outdated files and fix permissions.
Guillaume Melquiond
2015-07-31
*
Update headers.
Maxime Dénès
2015-01-12
*
Added an arithmetical characterization of the hypothesis of WKL.
Hugo Herbelin
2014-12-01
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
*
Make sure that Logic/ExtensionalityFacts gets compiled.
Guillaume Melquiond
2014-10-27
*
Fix some typos.
Guillaume Melquiond
2014-10-27
*
Fix some typos in comments.
Guillaume Melquiond
2014-10-27
*
EqdepFacts: generalize statements which were wrongly restricted to Prop.
Arnaud Spiwack
2014-10-22
*
ConstructiveEpsilon: simplify the before_witness type using non-uniform param...
Arnaud Spiwack
2014-10-16
*
Hurkens.v: Fix a syntax error.
Arnaud Spiwack
2014-09-26
*
ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...
Arnaud Spiwack
2014-09-26
*
Hurkens.v: new paradox: type of modal propositions is not a retract.
Arnaud Spiwack
2014-09-26
*
Hurkens.v: fix coqdoc formatting in a comment.
Arnaud Spiwack
2014-09-26
*
Hurkens.v: update comments.
Arnaud Spiwack
2014-09-25
*
Return a Prop not an arbitrary Type, and correct a typo.
Matthieu Sozeau
2014-09-24
*
Hurkens.v: show proofs in coqdoc.
Arnaud Spiwack
2014-09-24
*
Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].
Arnaud Spiwack
2014-09-24
*
Hurkens.v: coqdoc documentation.
Arnaud Spiwack
2014-09-24
*
A new version of Hurkens.v.
Arnaud Spiwack
2014-09-24
*
Prove forall extensionality
Jason Gross
2014-08-26
*
sed s'/_one_var/_on/g'
Jason Gross
2014-08-26
*
Generalize EqdepFacts
Jason Gross
2014-08-26
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Completing c236b51348d2 by fixing EqdepFactsv actually committing the
Hugo Herbelin
2014-07-17
*
Added a (constructive) proof of Weak Konig's lemma for decidable trees.
Hugo Herbelin
2014-07-15
*
Some basics facts about eq_dep.
Hugo Herbelin
2014-07-15
*
Remove some theories that have been deprecated for 10 years.
Guillaume Melquiond
2014-06-26
*
Making those proofs which depend on names generated for the arguments
Hugo Herbelin
2014-06-01
[next]