coq - The formal proof system

Age	Commit message (Expand)	Author
2010-01-08	Init/Logic: commutativity and associativity of /\ and \/	letouzey
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-11-16	Some lemmas about dependent choice + extensions of Compare_dec +	herbelin
2009-11-06	Datatypes.length and app defined back via fun+fix instead of Fixpoint	letouzey
2009-11-03	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey
2009-11-02	Remove various useless {struct} annotations	letouzey
2009-11-02	list, length, app are migrated from List to Datatypes	letouzey
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-10-08	Implicit argument of Logic.eq become maximally inserted	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-24	New tactic to rewrite decidability lemmas when one knows which side	herbelin
2009-08-11	Fixed extra space in printing notation { x & P } + minor other things	herbelin
2009-07-24	OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith	letouzey
2009-06-29	Miscellaneous practical commits:	herbelin
2009-03-27	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-01-02	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-11-23	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-10-14	ugly comment erroneously left in the minus definition	letouzey
2008-08-05	Correction de bugs:	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-23	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin
2008-06-12	Changing the definitions of pred and minus in the style of GG	werner
2008-06-08	- Patch sur "intros until 0"	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-06-02	Petites corrections diverses :	herbelin
2008-05-28	- Modification de la déf de minus et pred conformément aux remarques de	herbelin
2008-05-28	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin
2008-05-12	MAJ et bricoles diverses	herbelin
2008-05-09	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin
2008-04-29	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-09	contradict can now handle False hypothesis in the spirit of contradiction	letouzey
2008-03-23	Nettoyage Wf.v et unification (suite remarques faites sur cocorico)	herbelin
2008-03-23	Une passe sur les réels:	herbelin
2008-03-15	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau
2008-03-07	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey
2008-03-04	still one more substituion s/Set/Type/	letouzey
2008-02-26	Proper implicit arguments handling for assumptions	msozeau
2008-01-23	Typo	notin
2007-12-17	Quelques arguments en plus...	glondu
2007-11-08	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov
2007-11-06	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey
2007-11-06	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey
2007-11-01	A way to specialize universally quantified hypothesis: if H is	letouzey