coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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-06
*	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-05-02
*	Fix Qcanon after changes on injection.	Maxime Dénès	2014-04-30
*	Import proof of decidability of negated formulas from Coquelicot.	Guillaume Melquiond	2014-04-23
*	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-22
*	Fixing missing headers.	Hugo Herbelin	2014-04-16
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Define [projT3] and [proj3_sig]	Jason Gross	2014-04-10
*	Closing bug #3164	Julien Forest	2014-04-04
*	Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.	Guillaume Melquiond	2014-03-10
*	Pos.compare_cont takes the comparison as first argument	Pierre Boutillier	2014-02-28
*	fixup complement Fin	Pierre Boutillier	2014-02-24
*	Less dependencies in Omega.	Pierre-Marie Pédrot	2014-02-08
*	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey	2014-02-07
*	[Coercion]s use [Sortclass], not [Prop] (in docs)	Jason Gross	2014-01-24
*	List: Bug 3039 weaker requirement for fold symmetric	Pierre Boutillier	2013-12-20
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Generalize eq_proofs_unicity	Jason Gross	2013-12-12
*	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-04
*	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-12-03
*	Adding Acc_intro_generator in order to help computations of Function in parti...	forest	2013-11-20
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	Restore Zsqrt compat now that refine works fine with match.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge	2013-08-08
*	Adding a dependent version of equal_f, thus fixing #3074.	ppedrot	2013-08-02
*	Typo in definition clos_refl	ppedrot	2013-07-31
*	Fixing #3089. This implied tweaking the definition of the lexicographic	ppedrot	2013-07-26
*	Added a concat function to List theory. Strangely, it was missing.	ppedrot	2013-07-24
*	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	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-06-02
*	Improving printing of 'rew' notation	herbelin	2013-05-05
*	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin	2013-05-05
*	Added group properties of eq_refl, eq_sym, eq_trans	herbelin	2013-04-17
*	Normalized type for Vector.map2	pboutill	2013-03-25
*	NMake*: avoid some warning about Let outside sections	letouzey	2013-03-22