aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2015-08-29Adding a proof of surjective pairing on vectors.Hugo Herbelin
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Adding a notation { x & P } for { x : _ & P }.Hugo Herbelin
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-12The "on_last_hyp" tactic now behaves as it should.Cyprien Mangin
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-12List.nth_error directly produces Some/None instead of value/errorPierre Letouzey
2015-05-12Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Guillaume Melquiond
2015-05-09Tentatively setting cons and Some with 1st implicit argument maximalHugo Herbelin
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-09Prove [map_ext] using [map_ext_in].Nickolai Zeldovich
2015-04-09Add a [map_ext_in] lemma to List.v.Nickolai Zeldovich
2015-04-09Fix instances of universe-polymorphic generalized rewriting to avoidMatthieu Sozeau
2015-04-02MMapAVL: some improved proofs + fix a forgotten AdmittedPierre Letouzey
2015-04-02MMapAVL: implementing MMapInterface via AVL treesPierre Letouzey
2015-04-02ZArith/Int.v: some modernizationsPierre Letouzey
2015-04-02MMapPositive: some improvementsPierre Letouzey
2015-04-01Accomodating #4166 (providing "Require Import OmegaTactic" as aHugo Herbelin
2015-03-31Fix various typos in documentationMatěj Grabovský
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-06Add some missing Proof keywords.Guillaume Melquiond
2015-03-06Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-06MMapPositive: another implementation of MMapsPierre Letouzey
2015-03-05Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-05MMaps again : adding MMapList, an implementation by ordered listPierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-26Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Maxime Dénès
2015-02-25Reorder the steps of the easy tactic. (Fix for bug #2630)Guillaume Melquiond
2015-02-23Merge branch 'v8.5' into trunkEnrico Tassi
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-16Fixing bug #4035 (support for dependent destruction within ltac code).Hugo Herbelin
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
2015-01-18Merge branch '8.5' into trunkMatthieu Sozeau
2015-01-18Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-18Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Matthieu Sozeau
2015-01-18Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-18There was one more universe needed due to the use of now non-universe-polymor...Matthieu Sozeau
2015-01-16Add two lemmas about firstn to the List standard library.Sébastien Hinderer
2015-01-16Lemmas related to the firstn function over lists.Sébastien Hinderer
2015-01-16ListSet: follow-up of Sebastien's last commitPierre Letouzey
2015-01-16Work in progress on listset.Sébastien Hinderer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:03:04 +0000