coq - The formal proof system

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