| Age | Commit message (Expand) | Author |
|---|
| 2013-06-02 | A constructive proof of Fan theorem where paths are represented by predicates. | herbelin |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2013-05-05 | Improving printing of 'rew' notation | herbelin |
| 2013-05-05 | Relaxing the constraint on eta-expanding on the fly while looking for | herbelin |
| 2013-04-17 | Added group properties of eq_refl, eq_sym, eq_trans | herbelin |
| 2013-03-25 | Normalized type for Vector.map2 | pboutill |
| 2013-03-22 | NMake*: avoid some warning about Let outside sections | letouzey |
| 2013-03-21 | Using hnf instead of "intro H" for forcing reduction to a product. | herbelin |
| 2013-02-25 | cbn friendly VectorDef | pboutill |
| 2013-02-13 | make validate repaired via a temporary fix for #2949 | letouzey |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-12-21 | nat_iter n f x -> nat_rect _ x (fun _ => f) n | pboutill |
| 2012-12-18 | 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-08 | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau |
| 2012-12-05 | Making subset_eq_compat applying over more general domain "Type" (see #2938). | herbelin |
| 2012-12-04 | Identities over types satisfying Uniqueness of Identity Proofs | herbelin |
| 2012-11-15 | 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-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 |
