| Commit message (Expand) | Author | Age |
|---|
| * | Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing |  herbelin | 2012-11-15 |
| * | Some lemmas on property of rewriting. It will probably be worth at | herbelin | 2012-11-15 |
| * | Added a proof that Prop<>Type, for arbitrary fixed Type. | herbelin | 2012-11-15 |
| * | A decidability property of functional relations over decidable codomains. | herbelin | 2012-11-15 |
| * | For the record, two examples of short proofs of uniqueness of identity | herbelin | 2012-11-15 |
| * | Change Hint Resolve, Immediate to take a global reference as argument |  msozeau | 2012-10-26 |
| * | Removed a few calls to "Opaque" in Logic.v ineffective since at least | herbelin | 2012-10-24 |
| * | Removing redundant definition of case_eq (see #2919). | herbelin | 2012-10-16 |
| * | 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-04 |
| * | Ltac repeat is in fact already doing progress |  letouzey | 2012-10-01 |
| * | No more states/initial.coq, instead coqtop now requires Prelude.vo | letouzey | 2012-08-23 |
| * | fast bitwise operations (lor,land,lxor) on int31 and BigN | letouzey | 2012-08-11 |
| * | Updating headers. | herbelin | 2012-08-08 |
| * | MSetRBT: a tail-recursive plength | letouzey | 2012-08-06 |
| * | Same for Fin |  pboutill | 2012-07-25 |
| * | Vector equalities first stuff | pboutill | 2012-07-20 |
| * | isolate instances about Permutation and PermutationA which may slow rewrite | letouzey | 2012-07-10 |
| * | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey | 2012-07-09 |
| * | 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-06 |
| * | 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-07-05 |
| * | Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ... | pboutill | 2012-06-20 |
| * | Fix bug #2695: infinite loop in dependent destruction. | msozeau | 2012-06-19 |
| * | BinInt: a forgotten scope for a notation | letouzey | 2012-06-19 |
| * | 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-11 |
| * | Modifications and rearrangements to remove the action that sin (PI/2) = 1 | bertot | 2012-06-05 |
| * | list_eq_dec now transparent (wish #2786) | letouzey | 2012-06-01 |
| * | Functions *_beq aren't generated anymore, remove comments about them | letouzey | 2012-05-30 |
| * | Bugs revealed by playing with contribs | pboutill | 2012-05-25 |
| * | 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-22 |
| * | List + Permutation : more results about nth_error and nth | letouzey | 2012-05-18 |
| * | Intuition: temporary(?) restore the unconditional unfolding of not | letouzey | 2012-05-15 |
| * | Vectors takes advantage of pattern matching compiler fixup | pboutill | 2012-05-11 |
| * | Bug 2767 | pboutill | 2012-05-09 |
| * | Coqide highligthing is back (done by gtksourceview). | pboutill | 2012-05-02 |
| * | A notion of permutation for lists modulo a setoid equality | letouzey | 2012-05-02 |
| * | remove undocumented and scarcely-used tactic auto decomp | letouzey | 2012-04-23 |
| * | Remove the Dp plugin. |  gmelquio | 2012-04-17 |
| * | Fixing typo in previous commit r15180. | herbelin | 2012-04-15 |
herbelin
msozeau
letouzey
pboutill
bertot
gmelquio