coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
*	Nouvelle en-tête	herbelin	2004-07-16
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
*	Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...	herbelin	2004-04-08
*	Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)	herbelin	2004-04-06
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	Motifs recursifs de notations: prise en compte de l'associativite et des nota...	herbelin	2004-03-17
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	bug des points fixes (pb avec la contrib Matrices)	barras	2004-03-12
*	Correction d'un defaut dans la globalisation des variables de notations	herbelin	2004-03-12
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Prise en compte des implicites au travers des notations et abbreviations	herbelin	2004-02-28
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Localisation erreur interp_notation	herbelin	2004-02-12
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	reparation de qqs bugs du traducteur	barras	2004-01-26
*	Correction lecture des locations si pas demandees dans l'ordre	herbelin	2004-01-22
*	Export information des references de notations pour coqdoc	herbelin	2004-01-21
*	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin	2003-12-19
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin	2003-11-19
*	reparation bug moins unaire (erreur de PP)	barras	2003-11-18
*	Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...	herbelin	2003-11-17
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin	2003-10-14
*	Pb residuel avec la prise en compte des parametres implicites d'inductifs	herbelin	2003-10-08
*	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin	2003-10-08
*	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin	2003-09-29
*	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin	2003-09-26
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	Parsing correct des explicites en cas de projection	herbelin	2003-09-18
*	Scope type pour le codomaine de Prod aussi	herbelin	2003-09-12
*	Ajout If; synchro avec constrextern	herbelin	2003-09-09
*	cosmetique	herbelin	2003-09-06
*	Plus de passage du scope tmp sous les lambdas	herbelin	2003-09-02
*	Symetrisation des changements implicites de scope	herbelin	2003-08-31
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Hack pour ameliorer l'affichage des applications dans les `...` et	herbelin	2003-05-14
*	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin	2003-04-10
*	Mécanisme plus simple et efficace pour traduire les implicites	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Implicit Variables Type dans les inductive	herbelin	2003-03-29
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29