coq - The formal proof system

Age	Commit message (Expand)	Author
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-07-06	sequel to commit 9952: forgot to adapt xlate to the new n-ary rename	letouzey
2007-07-06	New intro pattern "@A", which generates a fresh name based on A.	glondu
2007-06-26	killing some more non-exhaustive patterns	letouzey
2007-05-25	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-29	Ajout possibilité d'options à trois mots.	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-02	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov
2007-03-19	Forgot to update to new cast	msozeau
2007-02-24	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin
2007-01-29	Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.	msozeau
2007-01-10	Merge from Lionel Elie Mamane's private branch:	lmamane
2007-01-10	Nouvelle approche pour le discharge modulaire	herbelin
2006-12-11	Changement dans le kernel :	bgregoir
2006-10-24	Extension de fresh (suite)	herbelin
2006-10-01	Une passe sur l'injection et la discrimination...	herbelin
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-01	Ajout possibilité clause "where" dans co-points fixes	herbelin
2006-08-22	making otags working	jforest
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-07-06	Suite remplacement VernacDebug par VernacSetOption	herbelin
2006-07-03	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin
2006-06-23	Suite passage ident -> hyp dans syntaxe de 'replace with in'	herbelin
2006-06-08	Changement du type d'argument 'TacticArgType X' en un type	herbelin
2006-06-08	DÃ©tection bug rawwit suitecorrection trou de typage create_arg	herbelin
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-21	+ destruct now works as induction on multiple arguments :	jforest
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-01-28	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2006-01-28	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin
2006-01-21	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin
2006-01-16	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin
2005-12-30	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Achèvement suppression traducteur dans contrib/interface	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-23	Simplifification de vernac_expr li l'abandon du traducteur	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-14	adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,	bertot
2005-05-20	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot