aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2012-05-09Bug 2767pboutill
2012-05-02Coqide highligthing is back (done by gtksourceview).pboutill
2012-05-02A notion of permutation for lists modulo a setoid equalityletouzey
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2012-04-17Remove the Dp plugin.gmelquio
2012-04-15Fixing typo in previous commit r15180.herbelin
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-03-26Fixing printing level of Utf8 equivalent for ->.herbelin
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-20Turning proofs of well-ordering of lexicographic product transparentherbelin
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Everything compiles again.msozeau
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-02-29Vector: missing injection lemmas and better impossible branchespboutill
2012-02-01Fix unblocking code in dependent destruction due to zeta being used in unfold...msozeau
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2012-01-23Deleted the only use of BeginSubProof from the standard library.ppedrot
2012-01-19No more use of tauto in Init/pboutill
2012-01-17MSetAVL: better implementation of filter suggested by X. Leroyletouzey
2012-01-13Added the decidability of (<=) on nat.ppedrot
2012-01-06Fixed the itarget of the previous commit...ppedrot
2012-01-06Added a typeclass-based system to reason on decidable propositions.ppedrot
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-12-07Vectors use a bit more the pattern matching compilerpboutill
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-21VectorDef.v takes benefit of dependencies being taken into accountherbelin
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-03Cleaning a little bit the files talking about descriptions: avoidingherbelin
2011-10-26Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).herbelin
2011-10-25Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).herbelin
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...msozeau
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
2011-10-10Proper fix for complement/flip instances.msozeau
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-10-05Removing vernacular code mistakenly committed.herbelin
2011-10-05Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...letouzey
2011-10-01Moving never-used comments from Zhints.v to dev/doc so as not toherbelin
2011-09-17Euclid: make the proof transparent (example of extraction in stdlib)letouzey
2011-09-16Omega: for non-arithmetical goals, try proving False from context (wish #2236)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:05:38 +0000