aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
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-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-06MMapPositive: another implementation of MMapsPierre Letouzey
2015-03-05MMaps again : adding MMapList, an implementation by ordered listPierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
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-23Fix some typos in comments.Guillaume Melquiond
2015-02-16Fixing bug #4035 (support for dependent destruction within ltac code).Hugo Herbelin
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
2015-01-18There was one more universe needed due to the use of now non-universe-polymor...Matthieu Sozeau
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-15Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Matthieu Sozeau
2015-01-15Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-28Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Arnaud Spiwack
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-12-18Adds two lemmas about hderror to the List standard library.Sébastien Hinderer
2014-12-18Implement the nodup function on lists and prove associated results.Sébastien Hinderer
2014-12-18Lists: enhanced version of Seb's last commit on Exists/ForallPierre Letouzey
2014-12-18Lists: a few results on Exists and Forall and a bit of code cleanup.Sébastien Hinderer
2014-12-15Failing on unbound notation variable in notation level modifiersHugo Herbelin
2014-12-11List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Pierre Letouzey
2014-12-11First series of results on lists.Sébastien Hinderer
2014-12-01Added an arithmetical characterization of the hypothesis of WKL.Hugo Herbelin
2014-11-18Clarifying the role of ListSet.v in the library, compared to otherHugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-02Improving elimination with indices, getting rid of intrusive residualHugo Herbelin
2014-11-02Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Hugo Herbelin
2014-10-27Make sure that Logic/ExtensionalityFacts gets compiled.Guillaume Melquiond
2014-10-27Fix some typos.Guillaume Melquiond
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-22EqdepFacts: generalize statements which were wrongly restricted to Prop.Arnaud Spiwack
2014-10-22Fixing typo absorption (bug #3751).Hugo Herbelin
2014-10-17Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Hugo Herbelin
2014-10-17Essai où assert_style n'est utilisé que si pas visuellement une équation;Hugo Herbelin
2014-10-16ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Arnaud Spiwack
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
2014-10-10Fix segfault in native compiler on int31 division.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 23:33:47 +0000