coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-30	Corrections dans le Print Assumption. Les definitions locales ("Let")	aspiwack
2007-05-29	Corrected the treatment of negative numbers for the bigZ parser. And	aspiwack
2007-05-28	Réaffichage des Structure/Record sous la forme Record	herbelin
2007-05-25	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles
2007-05-21	Added Z and Q implementations with int31.	aspiwack
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-15	Correction du pretty-printing des big-int (la sous-fonction get_height	aspiwack
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-05-10	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-29	Suite commit 9810	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-26	fin des conclusions multiples	corbinea
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-11	Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a	herbelin
2007-04-10	Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5	herbelin
2007-04-05	Mise en place d'un rafinement de compute.	jforest
2007-04-02	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov
2007-03-21	Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...	notin
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-02-24	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-16	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau
2007-02-15	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-01	Suppression de code mort	notin
2007-02-01	Abbreviation of order notation.	msozeau
2007-01-31	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-28	"suffices" implemented + syntax cleanup	corbinea
2007-01-25	decl mode: anonymous facts	corbinea
2007-01-22	Correction du bug #1315:	notin
2007-01-22	changes in declarative language : by term using tactic	corbinea
2007-01-11	Petit oubli dans commit 9474	herbelin
2007-01-10	Merge from Lionel Elie Mamane's private branch:	lmamane
2007-01-10	Nouvelle approche pour le discharge modulaire	herbelin
2006-12-23	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau
2006-12-12	nouvelle indentation des scripts	barras
2006-12-11	Changement dans le kernel :	bgregoir
2006-12-08	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-03	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin
2006-11-20	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-17	The emacs-U option now does not output any char above 250.	courtieu
2006-11-11	Fichiers obsolètes	herbelin
2006-11-02	gestion speciale du niveau 5 des ltac	barras
2006-10-31	syntaxe du let in encore	barras