coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-24	Ajout de la tactique "apply in".	herbelin
2006-10-24	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin
2006-10-24	Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...	herbelin
2006-10-23	fixed same_file (#1141)	barras
2006-10-23	fixed non-bug #1213	barras
2006-10-23	bug #1194: normalisation evars a la sortie de focus	barras
2006-10-23	Fixed "Show intros" which did not look at hypothesis.	courtieu
2006-10-23	Add a flush after backtracking x y z and before printing subgoals.	courtieu
2006-10-23	Add a flush for a warning.	courtieu
2006-10-21	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin
2006-10-21	Pas d'@ dans les identificateurs (pour F4 and co)	herbelin
2006-10-21	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin
2006-10-20	MAJ	herbelin
2006-10-20	Correction du bug #1255 (réécriture setoid sous un produit)	notin
2006-10-20	Correction de la localisation des erreurs en interactif (numéro de	herbelin
2006-10-20	Starting to add a function schemes merging command (not finished, not	courtieu
2006-10-19	Correction sym -> comm	herbelin
2006-10-19	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin
2006-10-17	field_simplify_eq profite de la factorisation de Laurent	barras
2006-10-17	Clarification des contraintes sur le contexte de paramètres des	herbelin
2006-10-17	Noms "canoniques" pour certaines des propriétés de xor.	herbelin
2006-10-17	Mise en forme des theories	notin
2006-10-16	affichage des ... dans les scripts	barras
2006-10-16	typo doc + bug legacy field	barras
2006-10-16	changes the use of lists and notations, to avoid that the notations	bertot
2006-10-13	Simplification ocamldebug (coq-debug-programs.out obsolète)	herbelin
2006-10-13	Ajout des options Coqide suggérées par Damien Doligez (wish #1053)	notin
2006-10-13	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin
2006-10-13	Correction test-suite suite à r9186	notin
2006-10-13	Ajout du théorème mult_minus_distr_l	notin
2006-10-13	r9778@tannat: jforest \| 2006-10-13 11:36:37 +0200	jforest
2006-10-12	Protection raise en début de séquence (en attendant que le code caché trou...	herbelin
2006-10-12	Fix name clash on left	thery
2006-10-11	Ajout de pages de man pour les exécutables coq	notin
2006-10-11	Ajout d'une option -annotate au configure+ changement du comportement par dé...	notin
2006-10-10	Fix 0 obligations bug	msozeau
2006-10-10	Remove duplicate conditions in Field + Monomial substitution function for PExpr	thery
2006-10-10	make sure BinList is not made visible to files that use the tactic Ring	bertot
2006-10-09	Exemple avec liaison des variables de filtrage du match	herbelin
2006-10-09	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin
2006-10-09	Notations:	herbelin
2006-10-09	Ajout combinateurs option_fold_left et name_fold_map	herbelin
2006-10-06	suite commit 9222 : rétablissement des tests autre que complexité	herbelin
2006-10-06	Remplacement des nf_evar (source de complexité polynomiale) par de la	herbelin
2006-10-06	Ajout d'un répertoire de test de la complexité	herbelin
2006-10-06	Déplacement de on_judgment_type de Typeops vers Termops	herbelin
2006-10-06	Suppression d'une source de complexité polynomiale dans le pretypage	herbelin
2006-10-06	MAJ	herbelin
2006-10-06	Annulation de l'essai de changement de sémantique du %scope (révision 9208).	herbelin
2006-10-05	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin