coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	Syntaxe IF then else au lieu de either and_then or_else	barras	2002-02-14
*	Raffinement library_part	herbelin	2002-02-12
*	petite modif pour ne pas expanser trop de let pendant l'unification	barras	2002-02-12
*	suppression de la condition de la permutation case/fun	letouzey	2002-02-12
*	pretty print	letouzey	2002-02-12
*	Test & correction de la production de code Haskell	letouzey	2002-02-12
*	Ajout library_part	herbelin	2002-02-12
*	substitution et pattern modulo let	barras	2002-02-11
*	bad printing of Zeta reduction flags (was missing)	barras	2002-02-11
*	mauvais comportement de l'inversion vis-a-vis des lets	barras	2002-02-08
*	prterm -> prterm_env	filliatr	2002-02-08
*	affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...	filliatr	2002-02-08
*	erreur mineure dans le test des inductifs imbriques	barras	2002-02-07
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	suppression du retour chariot a la fin de print_pure_constr	barras	2002-02-07
*	un assert false de trop (MLexn peut avoir des args)	letouzey	2002-02-07
*	oubli	letouzey	2002-02-06
*	gros changement dans mlutil.ml: ajout d'une elimination globale des prop	letouzey	2002-02-06
*	affichage des messages d'erreur pour Stack_overflow, Out_of_memory, Break	barras	2002-02-06
*	evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait	barras	2002-02-05
*	exclusion des rertoires de test de l'extraction	letouzey	2002-02-05
*	Ajout d'optimisations locales kill_prop	letouzey	2002-02-05
*	exceptionmal ratrappee	barras	2002-02-04
*	maj newsyntax	barras	2002-02-04
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01
*	adaptation de l'extraction aux changements de Christine concernant rec/rect e...	letouzey	2002-01-31
*	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring	2002-01-31
*	extraction des CoInductives via les Lazy d'ocaml	letouzey	2002-01-31
*	cosmetique	herbelin	2002-01-30
*	ajout list_split3, pr_semicolon et pr_bar	herbelin	2002-01-30
*	Reparation erreur de syntaxe	mohring	2002-01-30
*	modification de la definition des def inductives unitaires et autorisation d'...	mohring	2002-01-29
*	condition de positivite moins stricte vis-a-vis des parametres (cf bug de Edu...	barras	2002-01-29
*	Test affichage O de nat dans une expression sur Z	herbelin	2002-01-25
*	Bug affichage de O (de nat) dans une expression sur Z	herbelin	2002-01-25
*	* empty log message *	herbelin	2002-01-25
*	Zdiv et Zmod dans Zcomplements	filliatr	2002-01-25
*	patch Omega (bug 129)	filliatr	2002-01-25
*	Correction bug 'Check [b]if b then O else O'	herbelin	2002-01-25
*	Remplacement cut_intro par true_cut_anon pour Inversion	herbelin	2002-01-25
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-25
*	Correction de l'ordre des open (sachant que de toutes façons, un	herbelin	2002-01-24
*	Remplacement cut_intro par true_cut_anon	herbelin	2002-01-24
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-24
*	code mort	herbelin	2002-01-24
*	Cas LetIn superflu dans check_construct car normalisation préalable	herbelin	2002-01-24
*	Bug dépendances en les corps des let-in oubliées	herbelin	2002-01-24
*	Réparation bug 'known_dependent'	herbelin	2002-01-24
*	In Pcoq, the search commands had an erroneous behavior. Bound variables	bertot	2002-01-23