coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-15	Description of the new features of the module system (part two).	soubiran
2009-12-15	Description of the new features of the module system (first part).	soubiran
2009-12-14	Improved strategy for rewriting lemma possibly depending because of evars.	herbelin
2009-12-13	Addition of mergesort + cleaning of the Sorting library	herbelin
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin
2009-12-13	Completion of r12580 (better rendering of dependent rewrite and inversion).	herbelin
2009-12-13	Deactivating printing of {\| \|} for records when option Printing All is set.	herbelin
2009-12-13	Fixing bug in printing option as of remember and generalize	herbelin
2009-12-13	Revision 12557 continued (better rendering of dependent rewrite)	herbelin
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-12-12	Improved the rendering of "dependent rewrite" and hence of "inversion"	herbelin
2009-12-11	Deport the backtracking code out of the ide	vgross
2009-12-10	NZDomain: investigation of the shape of NZ domain, more results about ofnat:n...	letouzey
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-12-08	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey
2009-12-08	Fix the build of coq via ocamlbuild	letouzey
2009-12-08	integrate MSetToFiniteSet into the compilation (and fix it)	letouzey
2009-12-08	Sos.ml: no more warnings	letouzey
2009-12-08	Declaremods.ml: a useless function wrongly introduced in last commit	letouzey
2009-12-07	Fix bug #2197 (option show_toolbar not taken into account at startup)	vgross
2009-12-07	Remove the "detach script windows" feature.	vgross
2009-12-07	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey
2009-12-07	revert on commit r12553	barras
2009-12-06	Turn evars created by a tactic application into a subgoal immediately in	msozeau
2009-12-06	Forgot a file in last commit.	msozeau
2009-12-06	Fix anomaly when using typeclass resolution with filtered hyps in evars.	msozeau
2009-12-03	Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)	herbelin
2009-12-03	Restored rewriting of JMeq using JMeq_rect and co when the domains are the same	herbelin
2009-12-03	Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1	vgross
2009-12-03	declaremods.ml <--- code factoring	soubiran
2009-12-03	Rename proper to proper_prf to avoid clash with CoRN,	msozeau
2009-12-02	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin
2009-12-02	Remove interface plugin	glondu
2009-12-02	Update .gitignore	glondu
2009-12-01	two improvements of the guard condition:	barras
2009-12-01	fix coqchk options documentation	barras
2009-12-01	install manpage of coqchk	barras
2009-12-01	Fix make_exact_entry to allow applying [forall x, P x] hints directly,	msozeau
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-12-01	Fix bug in typeclass resolution. Better handling of universes in	msozeau
2009-11-30	Fix backtracking heuristic in typeclass resolution.	msozeau
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-27	Substitute terms for evars-as-goals as soon as they are solved in	msozeau
2009-11-26	svn:ignore property	herbelin
2009-11-26	Fixing xml theory file export (was not consistent with coqdoc file	herbelin
2009-11-25	Fix for notation scope & inductive types	vsiles
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-11-24	Small extra result on JMeq vs eq_dep.	herbelin
2009-11-23	Ergonomy and robustness fix	vgross