| Age | Commit message (Expand) | Author |
|---|
| 2014-01-24 | [Coercion]s use [Sortclass], not [Prop] (in docs) | Jason Gross |
| 2013-12-20 | List: Bug 3039 weaker requirement for fold symmetric | Pierre Boutillier |
| 2013-12-12 | Better unification for [projT1] and [proj1_sig]. | Jason Gross |
| 2013-12-12 | Generalize eq_proofs_unicity | Jason Gross |
| 2013-12-04 | Improved the presentation of the proof of UIP_refl_nat. | Hugo Herbelin |
| 2013-12-04 | Add lemma derivable_pt_lim_atan. | Guillaume Melquiond |
| 2013-12-03 | Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l. | Guillaume Melquiond |
| 2013-12-03 | Remove a useless hypothesis from Rle_Rinv. | Guillaume Melquiond |
| 2013-11-20 | Adding Acc_intro_generator in order to help computations of Function in parti... | forest |
| 2013-11-04 | Nicer infered names in refine. | aspiwack |
| 2013-11-02 | Restore Zsqrt compat now that refine works fine with match. | aspiwack |
| 2013-11-02 | A whole new implemenation of the refine tactic. | aspiwack |
| 2013-08-08 | Side effect free implementation of admit (Isabelle's oracle) | gareuselesinge |
| 2013-08-02 | Adding a dependent version of equal_f, thus fixing #3074. | ppedrot |
| 2013-07-31 | Typo in definition clos_refl | ppedrot |
| 2013-07-26 | Fixing #3089. This implied tweaking the definition of the lexicographic | ppedrot |
| 2013-07-24 | Added a concat function to List theory. Strangely, it was missing. | ppedrot |
| 2013-07-17 | "Boolean Equality" and "Case Analysis" are already off by default... | letouzey |
| 2013-07-17 | More dynamic argument scopes | letouzey |
| 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 |
