aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Bugs revealed by playing with contribsGravatar pboutill2012-05-25
* Permutation: remove a compatibility notation which doesn't help MathClassesGravatar letouzey2012-05-22
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
* Vectors takes advantage of pattern matching compiler fixupGravatar pboutill2012-05-11
* Bug 2767Gravatar pboutill2012-05-09
* Coqide highligthing is back (done by gtksourceview).Gravatar pboutill2012-05-02
* A notion of permutation for lists modulo a setoid equalityGravatar letouzey2012-05-02
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* Remove the Dp plugin.Gravatar gmelquio2012-04-17
* Fixing typo in previous commit r15180.Gravatar herbelin2012-04-15
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
* Uniformisation in the documentation: remove the use of 'coinductive' inGravatar aspiwack2012-04-13
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* Fixing printing level of Utf8 equivalent for ->.Gravatar herbelin2012-03-26
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Turning proofs of well-ordering of lexicographic product transparentGravatar herbelin2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* Vector: missing injection lemmas and better impossible branchesGravatar pboutill2012-02-29
* Fix unblocking code in dependent destruction due to zeta being used in unfold...Gravatar msozeau2012-02-01
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...Gravatar msozeau2012-01-28
* Deleted the only use of BeginSubProof from the standard library.Gravatar ppedrot2012-01-23
* No more use of tauto in Init/Gravatar pboutill2012-01-19
* MSetAVL: better implementation of filter suggested by X. LeroyGravatar letouzey2012-01-17
* Added the decidability of (<=) on nat.Gravatar ppedrot2012-01-13
* Fixed the itarget of the previous commit...Gravatar ppedrot2012-01-06
* Added a typeclass-based system to reason on decidable propositions.Gravatar ppedrot2012-01-06
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* Vectors use a bit more the pattern matching compilerGravatar pboutill2011-12-07
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* VectorDef.v takes benefit of dependencies being taken into accountGravatar herbelin2011-11-21
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Cleaning a little bit the files talking about descriptions: avoidingGravatar herbelin2011-11-03
* Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).Gravatar herbelin2011-10-26
* Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).Gravatar herbelin2011-10-25
* Fixing Equality.injectable which did not detect an equality withoutGravatar herbelin2011-10-22
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightGravatar letouzey2011-10-14
* Proper fix for complement/flip instances.Gravatar msozeau2011-10-10
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07