| Commit message (Expand) | Author | Age |
|---|
| * | make validate repaired via a temporary fix for #2949 |  letouzey | 2013-02-13 |
| * | Unset Asymmetric Patterns |  pboutill | 2013-01-18 |
| * | nat_iter n f x -> nat_rect _ x (fun _ => f) n | pboutill | 2012-12-21 |
| * | Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904) | letouzey | 2012-12-18 |
| * | No more constant named "int" in Coq theories (cf bug #2878) | letouzey | 2012-12-18 |
| * | Finish patch for Hint Resolve, stopping to generate new constant names for |  msozeau | 2012-12-08 |
| * | Making subset_eq_compat applying over more general domain "Type" (see #2938). |  herbelin | 2012-12-05 |
| * | Identities over types satisfying Uniqueness of Identity Proofs | herbelin | 2012-12-04 |
| * | 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 |
letouzey
pboutill
msozeau
herbelin
bertot