coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Un Local construit par preuve hors section doit être considéré global	herbelin	2002-11-06
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Nouvelle option -xml à coqtop pour compiler un développement en	herbelin	2002-11-05
*	Optimisation du choix des niveaux intermédiaires dans une notation complexe	herbelin	2002-10-30
*	code mort	herbelin	2002-10-26
*	Clarification changements autour de Remark/Fact/Local	herbelin	2002-10-23
*	Le test de redondance d'une règle était trop fort	herbelin	2002-10-23
*	Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...	herbelin	2002-10-22
*	Prise en compte des délimiteurs dans les motifs de Cases	herbelin	2002-10-21
*	Réparation du mécanisme des infixes quand ils commencent par une lettre	herbelin	2002-10-16
*	Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pas	herbelin	2002-10-14
*	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin	2002-10-14
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras	2002-10-09
*	Que des niveaux d'univers frais dans le type des constantes globales	herbelin	2002-09-29
*	Que des niveaux d'univers frais dans le type des constantes globales	herbelin	2002-09-29
*	Encore quelques rangements dans Nametab + petits trucs	coq	2002-09-27
*	Nametab data structure reorganisation	coq	2002-09-24
*	La notation with dependante + affichage dependante de moduels corrige	coq	2002-09-20
*	pretyping/pretyping.ml	herbelin	2002-09-03
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
*	Suppression automatique du corps des définitions locales opaques dans	herbelin	2002-08-17
*	Strengthenning rules for modules + No modules in sections	coq	2002-08-16
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Petites corrections ici et la	coq	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Error_in_file redondant et inapproprié	herbelin	2002-07-11
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Ajout de FNL ou utilisation de msgnl	herbelin	2002-06-07
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Fichier des expressions de commandes vernaculaires	herbelin	2002-05-29
*	Utilisation des de Bruijn pour la constructions des records et de leur projec...	herbelin	2002-05-13
*	Déplacement/renommage de Class.stre_max en Declare.strength_min	herbelin	2002-04-16
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	backtrack dans l'algo d'unification	barras	2002-04-10
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
*	Bug d'affichage des erreurs localisées dans un fichier suite à	herbelin	2002-03-27
*	Meilleure gestion de la reduction dans Field	delahaye	2002-03-17
*	raccourci -l en plus de -load-vernac-source	letouzey	2002-03-07
*	-dump-glob dans le usage	filliatr	2002-02-27
*	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr	2002-02-20
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	affichage des messages d'erreur pour Stack_overflow, Out_of_memory, Break	barras	2002-02-06
*	Plusieurs arguments autorisés pour Require et Read Module	herbelin	2002-01-18
*	Un ++ au lieu d'un ;	herbelin	2001-12-21