aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* List: Bug 3039 weaker requirement for fold symmetricGravatar Pierre Boutillier2013-12-20
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
* Generalize eq_proofs_unicityGravatar Jason Gross2013-12-12
* Improved the presentation of the proof of UIP_refl_nat.Gravatar Hugo Herbelin2013-12-04
* Add lemma derivable_pt_lim_atan.Gravatar Guillaume Melquiond2013-12-04
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Remove a useless hypothesis from Rle_Rinv.Gravatar Guillaume Melquiond2013-12-03
* Adding Acc_intro_generator in order to help computations of Function in parti...Gravatar forest2013-11-20
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
* Restore Zsqrt compat now that refine works fine with match.Gravatar aspiwack2013-11-02
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
* Typo in definition clos_reflGravatar ppedrot2013-07-31
* Fixing #3089. This implied tweaking the definition of the lexicographicGravatar ppedrot2013-07-26
* Added a concat function to List theory. Strangely, it was missing.Gravatar ppedrot2013-07-24
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* More dynamic argument scopesGravatar letouzey2013-07-17
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Improving printing of 'rew' notationGravatar herbelin2013-05-05
* Relaxing the constraint on eta-expanding on the fly while looking forGravatar herbelin2013-05-05
* Added group properties of eq_refl, eq_sym, eq_transGravatar herbelin2013-04-17
* Normalized type for Vector.map2Gravatar pboutill2013-03-25
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
* cbn friendly VectorDefGravatar pboutill2013-02-25
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* Making subset_eq_compat applying over more general domain "Type" (see #2938).Gravatar herbelin2012-12-05
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
* Isolating the ingredients of the proof of Prop<>Type (r15973). SeeingGravatar herbelin2012-11-15
* Some lemmas on property of rewriting. It will probably be worth atGravatar herbelin2012-11-15
* Added a proof that Prop<>Type, for arbitrary fixed Type.Gravatar herbelin2012-11-15
* A decidability property of functional relations over decidable codomains.Gravatar herbelin2012-11-15
* For the record, two examples of short proofs of uniqueness of identityGravatar herbelin2012-11-15
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Removed a few calls to "Opaque" in Logic.v ineffective since at leastGravatar herbelin2012-10-24
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
* Revert "En cours pour 'generalize in clause' et 'induction in clause'"Gravatar herbelin2012-10-04
* En cours pour 'generalize in clause' et 'induction in clause'Gravatar herbelin2012-10-04
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* MSetRBT: a tail-recursive plengthGravatar letouzey2012-08-06