coq - The formal proof system

Age	Commit message (Expand)	Author
2014-06-26	Deactivate the "Standard Propositions Naming" flag, source of a lot of	Hugo Herbelin
2014-06-20	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau
2014-06-04	Make standard library independent of the names generated by	Hugo Herbelin
2014-06-04	Make standard library independent of the names generated by	Hugo Herbelin
2014-06-04	Small lemma about Relations.	Hugo Herbelin
2014-06-04	Remove spurious Show in script.	Matthieu Sozeau
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-31	Basic lemmas about the algebraic structure of equality.	Hugo Herbelin
2014-05-26	Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q	Pierre Boutillier
2014-05-26	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau
2014-05-20	Moving (e)transitivity out of the AST.	Pierre-Marie Pédrot
2014-05-18	Revert "Fix Qcanon after changes on injection."	Maxime Dénès
2014-05-16	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-09	Update and start testing rewrite-in-type code.	Matthieu Sozeau
2014-05-09	Restore implicit arguments of irreflexivity (fixes bug #3305).	Matthieu Sozeau
2014-05-07	Removing comment outdated since eta holds in conversion rule (this	Hugo Herbelin
2014-05-06	Fix after merge.	Matthieu Sozeau
2014-05-06	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau
2014-05-06	Try a new way of handling template universe levels	Matthieu Sozeau
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