coq - The formal proof system

Age	Commit message (Expand)	Author
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-09-04	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin
2007-08-30	Oubli dans commit 10102...	herbelin
2007-08-29	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin
2007-08-24	Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...	herbelin
2007-08-22	- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)	herbelin
2007-07-18	Affichage de "thesis" seulement en mode déclaratif	herbelin
2007-07-16	Generalized CAMLP4USE for pp dependencies	corbinea
2007-07-13	New bootstrapping, improved, Makefile system	corbinea
2007-07-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-07-09	More natural notation for intro pattern: @a -> ?a	glondu
2007-07-06	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-06-30	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-26	killing some more non-exhaustive patterns	letouzey
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