coq - The formal proof system

Age	Commit message (Expand)	Author
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
2007-10-05	Added the automatic generation of the boolean equality if possible and the	vsiles
2007-10-03	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-08-08	Fix dependency bugs due to Program modules renamings.	msozeau
2007-08-07	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau
2007-06-22	Ajout exist & cie à la table des hints par symétrie avec ex_intro &	herbelin
2007-06-08	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov
2007-06-05	Gestion espaces dans notation _ = _ :> _	herbelin
2007-04-28	Déplacement des opérations sur bool dans l'état initial	herbelin
2007-04-02	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov
2007-04-01	Removed the definition of extensions of apply to equivalences	emakarov
2007-03-30	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov
2007-03-26	stupid me: ?f two times in a pattern	letouzey
2007-01-02	Add f_equal case for 6 arguments.	msozeau
2006-10-24	Ajout de la tactique 'remember'	herbelin
2006-10-17	Mise en forme des theories	notin
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-09-22	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin
2006-09-21	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey
2006-08-28	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin
2006-06-25	repetition d'hypotheses dans well_founded_induction_type_2	letouzey
2006-06-09	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin
2006-06-04	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin