| Age | Commit message (Expand) | Author |
|---|
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-24 | Removed a few calls to "Opaque" in Logic.v ineffective since at least | herbelin |
| 2012-10-16 | Removing redundant definition of case_eq (see #2919). | herbelin |
| 2012-10-04 | Revert "En cours pour 'generalize in clause' et 'induction in clause'" | herbelin |
| 2012-10-04 | En cours pour 'generalize in clause' et 'induction in clause' | herbelin |
| 2012-10-01 | Ltac repeat is in fact already doing progress | letouzey |
| 2012-08-23 | No more states/initial.coq, instead coqtop now requires Prelude.vo | letouzey |
| 2012-08-11 | fast bitwise operations (lor,land,lxor) on int31 and BigN | letouzey |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-06 | MSetRBT: a tail-recursive plength | letouzey |
| 2012-07-25 | Same for Fin | pboutill |
| 2012-07-20 | Vector equalities first stuff | pboutill |
| 2012-07-10 | isolate instances about Permutation and PermutationA which may slow rewrite | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-06 | Two adaptations after the changes of level of -> | letouzey |
| 2012-07-06 | BinPos/BinInt/BinNat : fix some argument scopes | letouzey |
| 2012-07-06 | Restore the compatibility notation Compare.not_eq_sym | letouzey |
| 2012-07-05 | Legacy Ring and Legacy Field migrated to contribs | letouzey |
| 2012-07-05 | Some cleanup in recent proofs concerning pi | letouzey |
| 2012-07-05 | MSetRBT : elementary arith proofs instead of calls to lia | letouzey |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-07-05 | Notation: a new annotation "compat 8.x" extending "only parsing" | letouzey |
| 2012-06-20 | Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ... | pboutill |
| 2012-06-19 | Fix bug #2695: infinite loop in dependent destruction. | msozeau |
| 2012-06-19 | BinInt: a forgotten scope for a notation | letouzey |
| 2012-06-11 | These files are displaced from Rtrigo.v and Ranalysis_reg.v | bertot |
| 2012-06-11 | finish the rearrangement for removing the sin_PI2 axiom. This new version | bertot |
| 2012-06-11 | Adds the proof of PI_ineq, plus some other smarter ways to approximate PI | bertot |
| 2012-06-05 | Modifications and rearrangements to remove the action that sin (PI/2) = 1 | bertot |
| 2012-06-01 | list_eq_dec now transparent (wish #2786) | letouzey |
| 2012-05-30 | Functions *_beq aren't generated anymore, remove comments about them | letouzey |
| 2012-05-25 | Bugs revealed by playing with contribs | pboutill |
| 2012-05-22 | Permutation: remove a compatibility notation which doesn't help MathClasses | letouzey |
| 2012-05-22 | SetoidList: explicit the fact that InfA_compat won't use ltA_strorder | letouzey |
| 2012-05-18 | List + Permutation : more results about nth_error and nth | letouzey |
| 2012-05-15 | Intuition: temporary(?) restore the unconditional unfolding of not | letouzey |
| 2012-05-11 | Vectors takes advantage of pattern matching compiler fixup | pboutill |
| 2012-05-09 | Bug 2767 | pboutill |
| 2012-05-02 | Coqide highligthing is back (done by gtksourceview). | pboutill |
| 2012-05-02 | A notion of permutation for lists modulo a setoid equality | letouzey |
| 2012-04-23 | remove undocumented and scarcely-used tactic auto decomp | letouzey |
| 2012-04-17 | Remove the Dp plugin. | gmelquio |
| 2012-04-15 | Fixing typo in previous commit r15180. | herbelin |
| 2012-04-15 | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin |
| 2012-04-13 | MSetRBT : implementation of MSets via Red-Black trees | letouzey |
| 2012-04-13 | Uniformisation in the documentation: remove the use of 'coinductive' in | aspiwack |
| 2012-04-12 | "A -> B" is a notation for "forall _ : A, B". | pboutill |
| 2012-04-06 | Fixing a few bugs (see #2571) related to interpretation of multiple binders | herbelin |
