index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Logic
/
vo.itarget
Age
Commit message (
Expand
)
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
2017-03-19
Add a forgotten (?) line to "theories/Logic/vo.itarget".
Matej Kosik
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
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
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
2013-06-02
A constructive proof of Fan theorem where paths are represented by predicates.
herbelin
2009-12-09
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
