coq - The formal proof system

Age	Commit message (Expand)	Author
2006-02-12	Nettoyage Bool:	herbelin
2006-02-12	Unification max_case et max_case2	herbelin
2006-02-12	Unification min_case et min_case2	herbelin
2006-02-11	maj	coq
2006-02-11	Commentaires et compatibilité coqdoc	herbelin
2006-02-10	maj	coq
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-02-10	code mort	herbelin
2006-02-09	maj	coq
2006-02-09	very minor bug correction and cleanning	bertot
2006-02-09	securing intros (we now use h_intro)	bertot
2006-02-09	Minor bugs fixes	bertot
2006-02-08	maj	coq
2006-02-08	Changing Set to Type for iter.	bertot
2006-02-08	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot
2006-02-08	Julien:	bertot
2006-02-08	Localisation des erreurs de sorte du prétypage	herbelin
2006-02-08	Ajout bibliothèque String de Laurent Théry	herbelin
2006-02-08	Ajout bibliothèque String de Laurent Théry	herbelin
2006-02-07	maj	coq
2006-02-07	oubli de code de debugging	herbelin
2006-02-07	Messages nth branche	herbelin
2006-02-07	Idem numbering of 'Unfold', 'simpl', ...	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2006-02-07	Ajout plural	herbelin
2006-02-07	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin
2006-02-07	MAJ	herbelin
2006-02-06	maj	coq
2006-02-06	Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...	herbelin
2006-02-06	warning seulement si mode verbose	herbelin
2006-02-06	coq_makefile	herbelin
2006-02-06	Ajout de l'essai d'effacement des noms des cibles custom par la cible clean	herbelin
2006-02-05	maj	coq
2006-02-05	Debugging en syntaxe v8	herbelin
2006-02-04	maj	coq
2006-02-04	Branchement sur nouvelle interface de declare_numeral_interpreter	herbelin
2006-02-04	Recherche des global_reference paresseusement pour pouvoir interpréter	herbelin
2006-02-04	parsing/g_ascii_syntax.ml	herbelin
2006-02-04	Ajout nat_path et find_reference	herbelin
2006-02-04	Utilisation du section_path pour le parsing des notations primitives,	herbelin
2006-02-04	code mort	herbelin
2006-02-03	maj	coq
2006-02-03	added mli 's for the nex functional induction (forgotten last time).	coq
2006-02-03	+ Adding an error message when the function cannot be defined	bertot
2006-02-02	maj	coq
2006-02-01	maj	coq
2006-02-01	protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)	barras
2006-02-01	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