| Age | Commit message (Expand) | Author |
|---|
| 2015-09-08 | 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-08-29 | Adding a proof of surjective pairing on vectors. | Hugo Herbelin |
| 2015-08-14 | Move type_scope into user space, fix some output logs | Jason Gross |
| 2015-08-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross |
| 2015-08-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-08-02 | 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-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond |
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier |
| 2015-06-12 | The "on_last_hyp" tactic now behaves as it should. | Cyprien Mangin |
| 2015-05-15 | Merge v8.5 into trunk | Hugo Herbelin |
| 2015-05-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-09 | Tentatively setting cons and Some with 1st implicit argument maximal | Hugo Herbelin |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-05-01 | Giving to "subst" a more natural semantic (fixing #4214) by using all | Hugo Herbelin |
| 2015-04-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey |
| 2015-04-09 | 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-02 | 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-01 | Accomodating #4166 (providing "Require Import OmegaTactic" as a | Hugo Herbelin |
| 2015-03-31 | Fix various typos in documentation | Matěj Grabovský |
| 2015-03-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-03-06 | Add some missing Proof keywords. | Guillaume Melquiond |
| 2015-03-06 | Merge branch 'v8.5' into trunk | Pierre Letouzey |
| 2015-03-06 | MMapPositive: another implementation of MMaps | Pierre Letouzey |
| 2015-03-05 | Merge branch 'v8.5' into trunk | Pierre Letouzey |
| 2015-03-05 | MMaps again : adding MMapList, an implementation by ordered list | Pierre Letouzey |
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey |
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey |
| 2015-02-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-02-26 | Revert "Fixing bug #4035 (support for dependent destruction within ltac code)." | Maxime Dénès |
| 2015-02-25 | Reorder the steps of the easy tactic. (Fix for bug #2630) | Guillaume Melquiond |
| 2015-02-23 | Merge branch 'v8.5' into trunk | Enrico Tassi |
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond |
| 2015-02-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-02-16 | Fixing bug #4035 (support for dependent destruction within ltac code). | Hugo Herbelin |
| 2015-02-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-02-14 | dependent destruction: Fix (part of) bug #3961, by fixing dependent * | Matthieu Sozeau |
| 2015-01-18 | Merge branch '8.5' into trunk | Matthieu Sozeau |
| 2015-01-18 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-18 | Remove typeclass opaque directive, some proofs in the stdlib rely on it being... | Matthieu Sozeau |
| 2015-01-18 | Optionally allow eta-conversion during unification for type classes. | Matthieu Sozeau |
