coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin	2007-11-08
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	On Linux, we read /proc/self/exe to get the executable's path instead	glondu	2007-09-28
*	Modification of the Scheme command.	vsiles	2007-09-28
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin	2007-08-30
*	Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...	herbelin	2007-08-24
*	Utilisation plus précise de la contrainte de type pour interpréter les	herbelin	2007-08-24
*	Modification de l'initialisation des chemins de la librairie standard	notin	2007-08-20
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
*	If a fixpoint is not written with an explicit { struct ... }, then	letouzey	2007-07-07
*	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin	2007-06-30
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Contrôle de la compatibilité de apply via une information dans les	herbelin	2007-05-28
*	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles	2007-05-25
*	Nettoyage et standardisation des messages d'erreurs.	herbelin	2007-05-17
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin	2007-04-29
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	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-04-17
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	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-15
*	bug#1434 importing fonctor arguments, now it works.	soubiran	2007-03-09
*	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-24
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
*	Vérification que toutes les evars ont étés instanciées dans les types imp...	herbelin	2007-02-07
*	Tentative amélioration messages d'erreur prédicat d'élimination (cf notamment	herbelin	2007-01-24
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu	2006-12-28
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...	notin	2006-12-12
*	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
*	Fixed the -emacs option which was always On.	courtieu	2006-11-24
*	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin	2006-11-21
*	The emacs-U option now does not output any char above 250.	courtieu	2006-11-17
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	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