coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-25	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles
2007-05-17	Nettoyage et standardisation des messages d'erreurs.	herbelin
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-04-29	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-17	Reorder hook and printing of message, more natural this way.	msozeau
2007-04-17	Added the option to set/unset the automatic generation of elimination schemes	vsiles
2007-03-28	Support for implicit formal argument types in Program ; parse types in type s...	msozeau
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin
2007-03-15	Prévention notations récursives sans terminal à gauche et qui font boucler	herbelin
2007-03-09	bug#1434 importing fonctor arguments, now it works.	soubiran
2007-02-24	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin
2007-02-24	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin
2007-02-24	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin
2007-02-21	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin
2007-02-07	Vérification que toutes les evars ont étés instanciées dans les types imp...	herbelin
2007-01-24	Tentative amélioration messages d'erreur prédicat d'élimination (cf notamment	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-28	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu
2006-12-23	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau
2006-12-12	Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...	notin
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-11-24	Fixed the -emacs option which was always On.	courtieu
2006-11-21	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin
2006-11-17	The emacs-U option now does not output any char above 250.	courtieu
2006-11-02	gestion speciale du niveau 5 des ltac	barras
2006-10-28	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-23	bug #1194: normalisation evars a la sortie de focus	barras
2006-10-23	Add a flush after backtracking x y z and before printing subgoals.	courtieu
2006-10-20	Correction de la localisation des erreurs en interactif (numéro de	herbelin
2006-10-09	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin
2006-10-05	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin
2006-09-29	Added a new option -emacs-U changing emacs prompt delimiters by	courtieu
2006-09-25	Corrections mineures	notin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-15	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-12	Indentation + svnprop	notin
2006-09-09	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin
2006-09-06	Finalement, interdiction des points fixes non totalement mutuellement	herbelin
2006-09-01	Ajout possibilité clause "where" dans co-points fixes	herbelin