coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-21	Patches and instructions to enable Input Method support in CoqIDE.	vgross
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-21	In "progress", extending the set of evars w/o solving an existing one is	herbelin
2009-12-20	* Rewrite [classify_unicode] using standard unicode tables.	regisgia
2009-12-19	Backtrack on making exact hints for lemmas starting with products	msozeau
2009-12-19	Made the interpretation levels rlevel/glevel/tlevel truly phantom	herbelin
2009-12-18	RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd	letouzey
2009-12-18	Const_omega: look for S in Init only (avoid future clash with S of Numbers)	letouzey
2009-12-17	ZOdiv: fully use generic properties from ZDivTrunc.v	letouzey
2009-12-17	Reverse order of arguments in min_case_strong for better uniformity (and comp...	letouzey
2009-12-17	Division in Numbers : more properties, new filenames based on a paper by R. B...	letouzey
2009-12-16	correction de la nouvelle option pour functional induction	jforest
2009-12-16	adding an option functional_induction_rewrite_dependent to make functional in...	jforest
2009-12-16	Division in Numbers: more properties proved (still W.I.P.)	letouzey
2009-12-15	A generic euclidean division in Numbers (Still Work-In-Progress)	letouzey
2009-12-15	file integrated into the archive by mistake	letouzey
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