coq/theories/Logic/vo.itarget, branch master The formal proof system Remove remaining vo.itarget files (obsolete since PR #499) 2017-06-10T14:13:54+00:00 Pierre Letouzey 2017-06-10T14:13:54+00:00 79c42e22dd5106dcb85229ceec75331029ab5486 






Fixing missing PropFacts.v in Logic/vo.itarget.
2017-03-28T14:32:25+00:00

Hugo Herbelin

2017-03-28T14:29:15+00:00

45985baf2262504a9fb8f24e7960caa9f11d29f3

This is while waiting for a possible different solution, if ever such
a different solution is adopted, since the coq.inria.fr/library has
currently a broken link and someone rightly complained about it.





This is while waiting for a possible different solution, if ever such
a different solution is adopted, since the coq.inria.fr/library has
currently a broken link and someone rightly complained about it.







Add a forgotten (?) line to "theories/Logic/vo.itarget".
2017-03-19T12:30:01+00:00

Matej Kosik

2017-03-19T12:11:41+00:00

2f3b7a1ee530f236a153c0971cd99680dcee9b10

The "theories/Logic/PropExtensionalityFacts.v" file was:
- compiled
- used in several places
but not actually installed.

This commit fixes that.





The "theories/Logic/PropExtensionalityFacts.v" file was:
- compiled
- used in several places
but not actually installed.

This commit fixes that.







Adding explicitly a file to work in the context of propositional extensionality.
2017-03-03T13:42:04+00:00

Hugo Herbelin

2016-10-02T18:27:59+00:00

4e85cc6e9792da116f1b20e484b2ce629c6f6865












Adding a file providing extensional choice (i.e. choice over setoids).
2017-03-03T13:41:33+00:00

Hugo Herbelin

2016-10-02T20:02:52+00:00

9c21392c7957a0a1a66e5269022d5991649a38b5

Also integrating suggestions from Théo.





Also integrating suggestions from Théo.







Make sure that Logic/ExtensionalityFacts gets compiled.
2014-10-27T09:32:11+00:00

Guillaume Melquiond

2014-10-27T09:29:17+00:00

b56ec63bf021a8dd95ce2eddc365115ce818a43e












Added a (constructive) proof of Weak Konig's lemma for decidable trees.
2014-07-15T16:15:52+00:00

Hugo Herbelin

2014-07-15T16:15:26+00:00

c236b51348d2a39d8f105ef0c4e8a53fabc6e285

Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.





Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.







Remove some theories that have been deprecated for 10 years.
2014-06-26T14:37:14+00:00

Guillaume Melquiond

2014-06-26T14:37:05+00:00

35c834548dcbd590f66f009017d2f88797dce882












FinFun.v: results about injective/surjective/bijective fonctions over finite domains
2014-02-07T10:50:26+00:00

Pierre Letouzey

2014-02-03T10:11:38+00:00

009fb68f0578e462b817f50772e2fba8d58c4f0d

 + Some extra results about NoDup, Fin.t, ...





 + Some extra results about NoDup, Fin.t, ...







A constructive proof of Fan theorem where paths are represented by predicates.
2013-06-02T21:42:14+00:00

herbelin

2013-06-02T21:42:14+00:00

fe008055f8adc7acd6af1483a8e7fef98d27e267

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7