coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)	barras	2006-02-01
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01
*	Optimisation filtrage sans lieurs (utile pour Ltac)	herbelin	2006-02-01
*	maj	coq	2006-01-31
*	Adaptation message d'erreur au cas des string	herbelin	2006-01-31
*	Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char	herbelin	2006-01-31
*	Ajout décidabilité	herbelin	2006-01-31
*	maj	coq	2006-01-30
*	Suppression fonctions d'interprétation du vieux Case	herbelin	2006-01-30
*	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin	2006-01-30
*	Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et de	herbelin	2006-01-30
*	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer	herbelin	2006-01-30
*	Fonctions retournant les arits des constructeurs et inductifs (suite)	herbelin	2006-01-30
*	Déplacement du test du bon nombre d'argument des constructeurs (et de	herbelin	2006-01-30
*	Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la	herbelin	2006-01-30
*	Fonctions retournant les arits des constructeurs et inductifs	herbelin	2006-01-30
*	Nettoyage warning (dont flush et affichage seulement si mode verbose)	herbelin	2006-01-30
*	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;	herbelin	2006-01-30
*	Ajout ppenv	herbelin	2006-01-30
*	Plutôt pas de contraction des match dans le déboggueur	herbelin	2006-01-30
*	maj	coq	2006-01-29
*	Documentation	herbelin	2006-01-29
*	Ajout printer Idset.t	herbelin	2006-01-29
*	Bug 'match x in I' (potentiellement utilisable comme cast)	herbelin	2006-01-29
*	MAJ (synonymes de Lemma; auto using)	herbelin	2006-01-29
*	Ajout syntaxe concrète Proposition, synonyme de Lemma	herbelin	2006-01-29
*	maj	coq	2006-01-28
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma	herbelin	2006-01-28
*	- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma	herbelin	2006-01-28
*	Correction bug Inspect introduit par le passage du discharge à une méthode ...	herbelin	2006-01-28
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
*	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin	2006-01-28
*	maj	coq	2006-01-27
*	maj	coq	2006-01-26
*	maj	coq	2006-01-25
*	exporting the global reference to the inductive " \/ " in coqlib and	bertot	2006-01-25
*	maj	coq	2006-01-24
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
*	maj	coq	2006-01-23
*	Oubli lors suppression traducteur	herbelin	2006-01-23
*	Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...	herbelin	2006-01-23
*	Precision	herbelin	2006-01-23
*	maj	coq	2006-01-22
*	Application de la suggestion de Nicolas Magaud (#1060)	herbelin	2006-01-22
*	maj	coq	2006-01-21
*	Variable inutilisée	herbelin	2006-01-21
*	Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...	herbelin	2006-01-21
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Ajout de la contrainte que l'assertion doit être complètement prouvée dans...	herbelin	2006-01-21