aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Removed a few calls to "Opaque" in Logic.v ineffective since at leastGravatar herbelin2012-10-24
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
* Revert "En cours pour 'generalize in clause' et 'induction in clause'"Gravatar herbelin2012-10-04
* En cours pour 'generalize in clause' et 'induction in clause'Gravatar herbelin2012-10-04
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* MSetRBT: a tail-recursive plengthGravatar letouzey2012-08-06
* Same for FinGravatar pboutill2012-07-25
* Vector equalities first stuffGravatar pboutill2012-07-20
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Two adaptations after the changes of level of ->Gravatar letouzey2012-07-06
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
* Restore the compatibility notation Compare.not_eq_symGravatar letouzey2012-07-06
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
* MSetRBT : elementary arith proofs instead of calls to liaGravatar letouzey2012-07-05
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...Gravatar pboutill2012-06-20
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
* These files are displaced from Rtrigo.v and Ranalysis_reg.vGravatar bertot2012-06-11
* finish the rearrangement for removing the sin_PI2 axiom. This new versionGravatar bertot2012-06-11
* Adds the proof of PI_ineq, plus some other smarter ways to approximate PIGravatar bertot2012-06-11
* Modifications and rearrangements to remove the action that sin (PI/2) = 1Gravatar bertot2012-06-05
* list_eq_dec now transparent (wish #2786)Gravatar letouzey2012-06-01
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30
* 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