coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras	2001-09-04
*	Parsing	herbelin	2001-08-10
*	Ajout add_prefix/add_suffix	herbelin	2001-08-01
*	Comentaire errone.	clrenard	2001-07-23
*	Nettoyage	herbelin	2001-07-21
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Ajout hashconsing univers	herbelin	2001-07-03
*	Depliage des let-in dans le test de garde	herbelin	2001-07-03
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	Normalisation du predicat synthetise pour les Case	clrenard	2001-06-20
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	option -quality	filliatr	2001-05-28
*	erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un Let	letouzey	2001-05-25
*	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin	2001-05-25
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Ajout d'une fonction de remplacement d'un sous-terme par un terme.	clrenard	2001-05-15
*	nettoyage extraction	filliatr	2001-05-09
*	Changement de la structure des points fixes	barras	2001-05-03
*	interdiction occ positives ET negatives dans Pattern	werner	2001-04-24
*	reduction des let in dans whd_programs	filliatr	2001-04-23
*	un typage sûr pour Goal et Check	filliatr	2001-04-20
*	to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...	herbelin	2001-04-15
*	Suppression de mk_constr qui ne respectait pas l'invariant des applications (...	herbelin	2001-04-15
*	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...	filliatr	2001-04-11
*	réparation Correctness; options Extraction (changement de syntaxe)	filliatr	2001-04-10
*	mise a jour pour ocamlweb	filliatr	2001-04-02
*	amelioration de la structure des univers	barras	2001-03-28
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
*	entetes	filliatr	2001-03-15
*	Prise en compte des Let dans l'instance des evars	herbelin	2001-03-14
*	Amélioration message d'erreur conditions de garde	herbelin	2001-03-12
*	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin	2001-03-11
*	corrections de bug de la reduction	barras	2001-03-08
*	compare_constr independent du groupement des applications.	barras	2001-03-08
*	réparation (?) discharge axiome	filliatr	2001-03-06
*	Re-Déplacement extended_rel_list	herbelin	2001-03-05
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	nouvelle implantation de la reduction	barras	2001-03-01
*	retire profile	mohring	2001-02-28
*	Changement de subst_meta	mohring	2001-02-28
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14
*	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr	2001-02-08
*	Chgt signature de type_of_existential	herbelin	2001-02-07
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...	herbelin	2001-01-31
*	make doc	herbelin	2001-01-27
*	Ajout alias mutual_inductive_path = section_path	herbelin	2001-01-27
*	Ajout global_vars_decl	herbelin	2001-01-24