coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction message d'erreur ltac et adoption du modèle de message de Tacinterp	herbelin	2006-03-04
*	Déplacement du test du bon nombre d'argument des constructeurs (et de	herbelin	2006-01-30
*	Nettoyage warning (dont flush et affichage seulement si mode verbose)	herbelin	2006-01-30
*	Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...	herbelin	2006-01-09
*	Enregistrement dans glob.dump des utilisations de notations numériques (qui ...	herbelin	2006-01-08
*	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin	2005-12-30
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Correction bugs commit précédent	herbelin	2005-12-22
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Changement des named_context	gregoire	2005-12-02
*	Correction de la correction du test sur le nombre de parametres d'une projection	herbelin	2005-11-19
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Conséquences nettoyage pretyping.ml	herbelin	2005-09-09
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Standardisation of function names about global references (especially, renami...	herbelin	2005-02-18
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	Suppression capture des variables par lieurs non liés dans Notation	herbelin	2004-11-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin	2004-08-23
*	Apply implicit types to local binders too	herbelin	2004-08-06
*	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