aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
* 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
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* 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
* 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
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* 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
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
* There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
* 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
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
* Clarifying the role of ListSet.v in the library, compared to otherGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Gravatar Arnaud Spiwack2014-10-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 02:59:34 +0000