coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	- Fix arity handling in retyping (de Bruijn bug!)	Matthieu Sozeau
2014-05-06	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau
2014-05-06	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau
2014-05-06	Fix issue #88: restrict_universe_context was wrongly forgetting about constra...	Matthieu Sozeau
2014-05-06	Restore reasonable performance by not allocating during universe checks,	Matthieu Sozeau
2014-05-06	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-05-02	Pos.iter arguments in a better order for cbn.	Pierre Boutillier
2014-05-02	Cbn is happier when ?SetPositive fixpoints have the set as recursive argument	Pierre Boutillier
2014-05-02	Eta contractions to please cbn	Pierre Boutillier
2014-04-30	Fix Qcanon after changes on injection.	Maxime Dénès
2014-04-23	Import proof of decidability of negated formulas from Coquelicot.	Guillaume Melquiond
2014-04-22	Remove some uses of excluded middle.	Guillaume Melquiond
2014-04-22	Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...	Guillaume Melquiond
2014-04-16	Fixing missing headers.	Hugo Herbelin
2014-04-10	No more Coersion in Init.	Pierre Boutillier
2014-04-10	Define [projT3] and [proj3_sig]	Jason Gross
2014-04-04	Closing bug #3164	Julien Forest
2014-03-10	Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.	Guillaume Melquiond
2014-02-28	Pos.compare_cont takes the comparison as first argument	Pierre Boutillier
2014-02-24	fixup complement Fin	Pierre Boutillier
2014-02-08	Less dependencies in Omega.	Pierre-Marie Pédrot
2014-02-07	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey
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