coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	Suggestion of additional syntax for intro patterns:	letouzey	2007-07-06
*	Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record	herbelin	2007-06-30
*	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin	2007-06-30
*	killing some more non-exhaustive patterns	letouzey	2007-06-26
*	Corrections dans le Print Assumption. Les definitions locales ("Let")	aspiwack	2007-05-30
*	Corrected the treatment of negative numbers for the bigZ parser. And	aspiwack	2007-05-29
*	Réaffichage des Structure/Record sous la forme Record	herbelin	2007-05-28
*	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles	2007-05-25
*	Added Z and Q implementations with int31.	aspiwack	2007-05-21
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Correction du pretty-printing des big-int (la sous-fonction get_height	aspiwack	2007-05-15
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Suite commit 9810	herbelin	2007-04-29
*	Ajout possibilité d'options à trois mots.	herbelin	2007-04-29
*	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-28
*	fin des conclusions multiples	corbinea	2007-04-26
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a	herbelin	2007-04-11
*	Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5	herbelin	2007-04-10
*	Mise en place d'un rafinement de compute.	jforest	2007-04-05
*	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov	2007-04-02
*	Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...	notin	2007-03-21
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
*	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau	2007-02-16
*	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin	2007-02-15
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Suppression de code mort	notin	2007-02-01
*	Abbreviation of order notation.	msozeau	2007-02-01
*	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea	2007-01-31
*	Fix order of wf and measure arguments, patch Program doc.	msozeau	2007-01-31
*	"suffices" implemented + syntax cleanup	corbinea	2007-01-28
*	decl mode: anonymous facts	corbinea	2007-01-25
*	Correction du bug #1315:	notin	2007-01-22
*	changes in declarative language : by term using tactic	corbinea	2007-01-22
*	Petit oubli dans commit 9474	herbelin	2007-01-11
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	nouvelle indentation des scripts	barras	2006-12-12