coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Suite ajout option -output-context	herbelin	2006-12-08
*	Ajout d'une option -output-context qui affiche le contexte en CCI pur à la	herbelin	2006-12-08
*	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin	2006-12-03
*	Correction boucle du parseur en cas de caractÃère non unicode	herbelin	2006-11-20
*	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin	2006-11-20
*	The emacs-U option now does not output any char above 250.	courtieu	2006-11-17
*	Fichiers obsolètes	herbelin	2006-11-11
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	syntaxe du let in encore	barras	2006-10-31
*	assouplissement de la syntaxe du let de ltac: t1 ; let in autorise	barras	2006-10-31
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	Exports manquants dans ring	barras	2006-10-29
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin	2006-10-28
*	Ajout option Set Printing Universes et amélioration affichage des univers	herbelin	2006-10-28
*	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin	2006-10-24
*	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin	2006-10-24
*	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin	2006-10-19
*	affichage des ... dans les scripts	barras	2006-10-16