coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...	herbelin	2004-12-30
*	Bug (cf #892)	herbelin	2004-12-06
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Suppression IsConjecture redondant avec Conjectural	herbelin	2004-10-11
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	Nouvelle en-tête	herbelin	2004-07-16
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	Export de l'information si un inductive est un record ou non (pour xml)	herbelin	2004-03-31
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin	2004-01-29
*	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin	2004-01-13
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti...	herbelin	2003-10-14
*	Admitted rendu independant de Conjecture: plus pratique en mode interactif	herbelin	2003-10-13
*	Bug introduit dans start_proof par le commit precedent	herbelin	2003-10-13
*	Protection contre les noms de lemmes existant deja	herbelin	2003-10-13
*	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin	2003-10-08
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...	herbelin	2003-09-16
*	Déplacement de Declare et déclarations des scopes d'argument dans Declare	herbelin	2003-09-12
*	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin	2003-09-06
*	Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...	herbelin	2003-08-31
*	Mise en place structure pour des 'arguments scope' dirigés par une classe	herbelin	2003-06-10
*	Possibilité de syntaxe conjointement à la définition des inductifs et des ...	herbelin	2003-05-21
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29
*	Ajout "at next level" dans Notation	herbelin	2003-04-17
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	Ajout d'un choix 'onlyparse'	herbelin	2003-03-31
*	Implicit Variables Type dans les inductive	herbelin	2003-03-29
*	Petit netoyage dans lib	coq	2002-12-19
*	Prise en compte des scopes traversés dans les notations	herbelin	2002-12-15
*	Code mort ?	herbelin	2002-12-09
*	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin	2002-11-26
*	Passage à une représentation des fixpoints plus primitive dans constr_expr ...	herbelin	2002-11-15
*	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
*	Clarification changements autour de Remark/Fact/Local	herbelin	2002-10-23
*	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