index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Remove Print Universe directive.
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Add compatibility files (feature 4319)
Jason Gross
2015-09-30
*
Emphasizing that eta for vectors is an instance of caseS, as pointed
Hugo Herbelin
2015-09-08
*
Minor modifications to WeakFanTheorem.
Hugo Herbelin
2015-09-08
*
Adding a proof of eta on Vector.t of non-zero size.
Hugo Herbelin
2015-09-08
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
*
Adding a notation { x & P } for { x : _ & P }.
Hugo Herbelin
2015-08-02
*
Remove some outdated files and fix permissions.
Guillaume Melquiond
2015-07-31
*
The "on_last_hyp" tactic now behaves as it should.
Cyprien Mangin
2015-06-12
*
List.nth_error directly produces Some/None instead of value/error
Pierre Letouzey
2015-05-12
*
Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)
Guillaume Melquiond
2015-05-12
*
Giving to "subst" a more natural semantic (fixing #4214) by using all
Hugo Herbelin
2015-05-01
*
Prove [map_ext] using [map_ext_in].
Nickolai Zeldovich
2015-04-09
*
Add a [map_ext_in] lemma to List.v.
Nickolai Zeldovich
2015-04-09
*
Fix instances of universe-polymorphic generalized rewriting to avoid
Matthieu Sozeau
2015-04-09
*
MMapAVL: some improved proofs + fix a forgotten Admitted
Pierre Letouzey
2015-04-02
*
MMapAVL: implementing MMapInterface via AVL trees
Pierre Letouzey
2015-04-02
*
ZArith/Int.v: some modernizations
Pierre Letouzey
2015-04-02
*
MMapPositive: some improvements
Pierre Letouzey
2015-04-02
*
Accomodating #4166 (providing "Require Import OmegaTactic" as a
Hugo Herbelin
2015-04-01
*
Fix various typos in documentation
Matěj Grabovský
2015-03-31
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Add some missing Proof keywords.
Guillaume Melquiond
2015-03-06
*
MMapPositive: another implementation of MMaps
Pierre Letouzey
2015-03-06
*
MMaps again : adding MMapList, an implementation by ordered list
Pierre Letouzey
2015-03-05
*
Introducing MMaps, a modernized FMaps.
Pierre Letouzey
2015-03-04
*
Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."
Maxime Dénès
2015-02-26
*
Reorder the steps of the easy tactic. (Fix for bug #2630)
Guillaume Melquiond
2015-02-25
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
Fixing bug #4035 (support for dependent destruction within ltac code).
Hugo Herbelin
2015-02-16
*
dependent destruction: Fix (part of) bug #3961, by fixing dependent *
Matthieu Sozeau
2015-02-14
*
There was one more universe needed due to the use of now non-universe-polymor...
Matthieu Sozeau
2015-01-18
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Remove typeclass opaque directive, some proofs in the stdlib rely on it being...
Matthieu Sozeau
2015-01-15
*
Optionally allow eta-conversion during unification for type classes.
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...
Arnaud Spiwack
2014-12-28
*
Forbid Require inside interactive modules and module types.
Maxime Dénès
2014-12-25
*
Adds two lemmas about hderror to the List standard library.
Sébastien Hinderer
2014-12-18
*
Implement the nodup function on lists and prove associated results.
Sébastien Hinderer
2014-12-18
*
Lists: enhanced version of Seb's last commit on Exists/Forall
Pierre Letouzey
2014-12-18
*
Lists: a few results on Exists and Forall and a bit of code cleanup.
Sébastien Hinderer
2014-12-18
*
Failing on unbound notation variable in notation level modifiers
Hugo Herbelin
2014-12-15
*
List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)
Pierre Letouzey
2014-12-11
*
First series of results on lists.
Sébastien Hinderer
2014-12-11
*
Added an arithmetical characterization of the hypothesis of WKL.
Hugo Herbelin
2014-12-01
*
Clarifying the role of ListSet.v in the library, compared to other
Hugo Herbelin
2014-11-18
*
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
[next]