aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'forge/v8.5'Gravatar Pierre Boutillier2015-06-22
|\
| * The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * List.nth_error directly produces Some/None instead of value/errorGravatar Pierre Letouzey2015-05-12
| * Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Gravatar Guillaume Melquiond2015-05-12
* | Tentatively setting cons and Some with 1st implicit argument maximalGravatar Hugo Herbelin2015-05-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * Prove [map_ext] using [map_ext_in].Gravatar Nickolai Zeldovich2015-04-09
| * Add a [map_ext_in] lemma to List.v.Gravatar Nickolai Zeldovich2015-04-09
| * Fix instances of universe-polymorphic generalized rewriting to avoidGravatar Matthieu Sozeau2015-04-09
| * MMapAVL: some improved proofs + fix a forgotten AdmittedGravatar Pierre Letouzey2015-04-02
| * MMapAVL: implementing MMapInterface via AVL treesGravatar Pierre Letouzey2015-04-02
| * ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
| * MMapPositive: some improvementsGravatar Pierre Letouzey2015-04-02
| * Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
| * Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-11
|\|
| * admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| * Add some missing Proof keywords.Gravatar Guillaume Melquiond2015-03-06
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-03-06
|\|
| * MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-03-05
|\|
| * MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
| * Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* | Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-26
|\|
| * Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
| * Reorder the steps of the easy tactic. (Fix for bug #2630)Gravatar Guillaume Melquiond2015-02-25
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-02-23
|\|
| * Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-18
|\|
| * Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-15
|\|
| * dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
* | Merge branch '8.5' into trunkGravatar Matthieu Sozeau2015-01-18
|\|
* | Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-18
* | Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Gravatar Matthieu Sozeau2015-01-18
* | Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-18
| * There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
* | Add two lemmas about firstn to the List standard library.Gravatar Sébastien Hinderer2015-01-16
* | Lemmas related to the firstn function over lists.Gravatar Sébastien Hinderer2015-01-16
* | ListSet: follow-up of Sebastien's last commitGravatar Pierre Letouzey2015-01-16
* | Work in progress on listset.Gravatar Sébastien Hinderer2015-01-16
| * Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| * Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Gravatar Matthieu Sozeau2015-01-15
| * Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Gravatar Arnaud Spiwack2014-12-28