coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	code mort	herbelin	2006-02-10
*	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-09
*	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-08
*	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-07
*	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-06
*	maj	coq	2006-02-05
*	Debugging en syntaxe v8	herbelin	2006-02-05
*	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-04
*	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-03
*	maj	coq	2006-02-02
*	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	2006-02-01
*	maj	coq	2006-01-31
*	Adaptation message d'erreur au cas des string	herbelin	2006-01-31
*	Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char	herbelin	2006-01-31
*	Ajout décidabilité	herbelin	2006-01-31
*	maj	coq	2006-01-30
*	Suppression fonctions d'interprétation du vieux Case	herbelin	2006-01-30
*	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin	2006-01-30