| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-10 | Remove remaining vo.itarget files (obsolete since PR #499) | Pierre Letouzey | |
| 2017-03-28 | Fixing missing PropFacts.v in Logic/vo.itarget. | Hugo Herbelin | |
| 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. | |||
| 2017-03-19 | Add a forgotten (?) line to "theories/Logic/vo.itarget". | Matej Kosik | |
| The "theories/Logic/PropExtensionalityFacts.v" file was: - compiled - used in several places but not actually installed. This commit fixes that. | |||
| 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 | |
| Also integrating suggestions from Théo. | |||
| 2014-10-27 | Make sure that Logic/ExtensionalityFacts gets compiled. | Guillaume Melquiond | |
| 2014-07-15 | Added a (constructive) proof of Weak Konig's lemma for decidable trees. | Hugo Herbelin | |
| Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem after all. | |||
| 2014-06-26 | Remove some theories that have been deprecated for 10 years. | Guillaume Melquiond | |
| 2014-02-07 | FinFun.v: results about injective/surjective/bijective fonctions over finite ↵ | Pierre Letouzey | |
| domains + Some extra results about NoDup, Fin.t, ... | |||
| 2013-06-02 | A constructive proof of Fan theorem where paths are represented by predicates. | herbelin | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵ | letouzey | |
| in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |