coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin	2006-01-21
*	Déplacement de pr_arg et pr_opt de Ppconstr vers Util	herbelin	2006-01-21
*	Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...	herbelin	2006-01-21
*	Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc	herbelin	2006-01-21
*	maj	coq	2006-01-20
*	Ajout de la contrainte de résoudre l'assertion dans 'assert by'	herbelin	2006-01-20
*	Test bug 983	herbelin	2006-01-20
*	* empty log message *	barras	2006-01-20
*	maj	coq	2006-01-19
*	Conséquences supplémentaires de la fin du support v7	herbelin	2006-01-19
*	Export eassumption	herbelin	2006-01-19
*	Extended Unicode support	herbelin	2006-01-19
*	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin	2006-01-19
*	maj	coq	2006-01-18
*	Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc...	herbelin	2006-01-18
*	Recursive Definition now supports functions with more than one argument.	coq	2006-01-18
*	maj	coq	2006-01-17
*	maj	coq	2006-01-16
*	dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmo	letouzey	2006-01-16
*	Version préliminaire d'inversion de la compilation du filtrage	herbelin	2006-01-16
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin	2006-01-16
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom	herbelin	2006-01-16