coq - The formal proof system

Age	Commit message (Expand)	Author
2006-09-25	Corrections mineures	notin
2006-09-25	Permet a un unfold de recevoir ses occurences a travers une variable Ltac.	letouzey
2006-09-24	Tentative d'amélioration du message d'erreur en cas de paramètre non laissé	herbelin
2006-09-24	Correction bug dans détection clause "in" mal formée quand le "in" est	herbelin
2006-09-23	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin
2006-09-23	Correction bug #1168 (dans les coercions de pattern, c'est le nombre	herbelin
2006-09-23	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin
2006-09-23	Wish #1187 granted (support for canonical structures that are records	herbelin
2006-09-23	Correction bug #1229 (toplevel "unresolved evar" fled through	herbelin
2006-09-23	Déplacement surround dans util.ml et parenthésage des déclarations	herbelin
2006-09-23	- Correction filtrage des notations impliquant un "match" : la présence	herbelin
2006-09-22	Protection List.fold_left2 (cf bug #1224)	herbelin
2006-09-22	Tout petit bug d'affichage dans constr_display (top_printers)	herbelin
2006-09-22	Test Tactic Notation	herbelin
2006-09-22	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin
2006-09-22	doc du nouveau ring	barras
2006-09-21	Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...	herbelin
2006-09-21	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey
2006-09-21	better scope/require managment (patch by Russel O'Connor)	letouzey
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-20	congruence doc update	corbinea
2006-09-19	Gestion des arguments implicites dans les Functions bien fondees	jforest
2006-09-19	added congruence improvement	corbinea
2006-09-18	correction of bug #1220	jforest
2006-09-18	Correction du bug #1215	notin
2006-09-16	Message modification in Function	jforest
2006-09-15	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin
2006-09-15	Minor bug correction in well-founded Function.	jforest
2006-09-15	MAJ	herbelin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-15	Débogage: ajout affichage contraintes d'unification	herbelin
2006-09-14	Bug dans configure (test best_compiler)	notin
2006-09-14	Correction du bug #1181	jforest
2006-09-14	Compilation de Coq sous Windows	notin
2006-09-14	mise en conformite des messages d'erreur de Function avec la doc.	jforest
2006-09-14	Modification de l'appel aux exécutables Caml	notin
2006-09-13	Abandon unification pattern des evars dans apply: combiné avec le	herbelin
2006-09-12	Indentation + svnprop	notin
2006-09-12	Correction conflit Meta/Evar dans commit précédent et extension au	herbelin
2006-09-12	Ajout unification pattern dans l'algorithme d'unification des	herbelin
2006-09-12	Ajout array_distinct	herbelin
2006-09-11	Ajout eassumption index	herbelin
2006-09-09	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin
2006-09-07	Updating the doc about Function and co	courtieu
2006-09-06	Finalement, interdiction des points fixes non totalement mutuellement	herbelin
2006-09-05	Code mort	herbelin
2006-09-05	Workaround Map.fold semantic change in ocaml-3.08.4 and higher.	msozeau
2006-09-04	Fix wrong order for building library, add informative messages.	msozeau
2006-09-01	New handling of obligations.	msozeau
2006-09-01	Correction bug d'ordonnancement des hyps d'induction dans induction/destruct	herbelin