coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte let-in	herbelin	2002-10-29
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-28
*	Nettoyage	herbelin	2002-10-12
*	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
*	Déplacement et export de type_of_global dans Global	herbelin	2001-11-09
*	corrections mineures suite au commit de restructuration du noyau	barras	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey	2001-10-30
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Protection contre des arguments farfelus pour les implicites manuels	herbelin	2001-09-21
*	entetes	filliatr	2001-03-15
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Ré-introduction des implicites à la volée dans la définition des inductifs	herbelin	2001-01-27
*	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr	2000-11-24
*	deplacement poly_args; iterateurs sur les segments	filliatr	2000-11-22
*	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
*	methode export	filliatr	2000-11-15
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	L'état implicite des définitions survivant au discharge redevient celui du ...	herbelin	2000-10-23
*	Renommage canonique :	herbelin	2000-10-18
*	Prise en compte de l'environnement dans le calcul des implicites	herbelin	2000-10-11
*	Correction incompatibilites dans la fn des types des inductifs	herbelin	2000-10-06
*	correction bug univers (dummy_univ)	filliatr	2000-10-06
*	Correction pour make doc	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin	2000-07-01
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
*	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin	2000-05-31
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
*	suppression de Fw pour les implicites	herbelin	2000-05-03
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
*	modules	filliatr	1999-12-12
*	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
*	- environment -> safe_environment	filliatr	1999-12-01
*	- Typing -> Safe_typing	filliatr	1999-12-01
*	module Termast	filliatr	1999-11-26
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
*	juste l'interface de Discharge	filliatr	1999-09-28
*	- un effort sur la doc (ocamlweb)	filliatr	1999-09-19