coq - The formal proof system

Age	Commit message (Expand)	Author
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-29	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-28	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-27	maj	coq
2006-01-26	maj	coq
2006-01-25	maj	coq
2006-01-25	exporting the global reference to the inductive " \/ " in coqlib and	bertot
2006-01-24	maj	coq
2006-01-24	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin
2006-01-23	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-22	maj	coq
2006-01-22	Application de la suggestion de Nicolas Magaud (#1060)	herbelin
2006-01-21	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-20	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-19	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-18	maj	coq
2006-01-18	Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc...	herbelin