aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2012-07-06BinPos/BinInt/BinNat : fix some argument scopesletouzey
2012-07-06Restore the compatibility notation Compare.not_eq_symletouzey
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05Some cleanup in recent proofs concerning piletouzey
2012-07-05MSetRBT : elementary arith proofs instead of calls to lialetouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-20Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...pboutill
2012-06-19Fix bug #2695: infinite loop in dependent destruction.msozeau
2012-06-19BinInt: a forgotten scope for a notationletouzey
2012-06-11These files are displaced from Rtrigo.v and Ranalysis_reg.vbertot
2012-06-11finish the rearrangement for removing the sin_PI2 axiom. This new versionbertot
2012-06-11Adds the proof of PI_ineq, plus some other smarter ways to approximate PIbertot
2012-06-05Modifications and rearrangements to remove the action that sin (PI/2) = 1bertot
2012-06-01list_eq_dec now transparent (wish #2786)letouzey
2012-05-30Functions *_beq aren't generated anymore, remove comments about themletouzey
2012-05-25Bugs revealed by playing with contribspboutill
2012-05-22Permutation: remove a compatibility notation which doesn't help MathClassesletouzey
2012-05-22SetoidList: explicit the fact that InfA_compat won't use ltA_strorderletouzey
2012-05-18List + Permutation : more results about nth_error and nthletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-05-11Vectors takes advantage of pattern matching compiler fixuppboutill
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 09:38:41 +0000