coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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