coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add the ability to specify the implicit status of section variables and	msozeau	2008-04-02
*	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau	2008-03-15
*	Implicit arguments in class field declarations	msozeau	2008-01-02
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Nouvelle en-tête	herbelin	2004-07-16
*	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin	2003-09-23
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin	2003-04-10
*	Synchronisation séparée des implicites pour l'affichage du traducteur;	herbelin	2003-04-09
*	Correction Show Implicits	herbelin	2003-04-09
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin	2002-12-02
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-28
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	GROS COMMIT:	barras	2001-11-05
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	entetes	filliatr	2001-03-15
*	Ré-introduction des implicites à la volée dans la définition des inductifs	herbelin	2001-01-27
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	implicites manuels	filliatr	2000-11-21
*	separation calcul des implicites et declaration des constantes / inductifs / ...	filliatr	2000-11-21
*	Ajout implicits_of_global + accès par noms longs	herbelin	2000-11-20
*	L'état implicite des définitions survivant au discharge redevient celui du ...	herbelin	2000-10-23
*	suppression de Fw pour les implicites	herbelin	2000-05-03
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
*	poursuite de Vernacentries	filliatr	1999-12-01
*	module Termast	filliatr	1999-11-26
*	- un effort sur la doc (ocamlweb)	filliatr	1999-09-19