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
*
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
*
Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".
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
*
Fixing typo absorption (bug #3751).
Hugo Herbelin
2014-10-22
*
Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...
Hugo Herbelin
2014-10-17
*
Essai où assert_style n'est utilisé que si pas visuellement une équation;
Hugo Herbelin
2014-10-17
*
ConstructiveEpsilon: simplify the before_witness type using non-uniform param...
Arnaud Spiwack
2014-10-16
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Give the same argument name for the record binder of type class
Matthieu Sozeau
2014-10-10
*
Fix segfault in native compiler on int31 division.
Maxime Dénès
2014-10-10
[next]