coq - The formal proof system

Age	Commit message (Expand)	Author
2001-05-28	option -quality	filliatr
2001-05-25	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-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-15	Ajout d'une fonction de remplacement d'un sous-terme par un terme.	clrenard
2001-05-09	nettoyage extraction	filliatr
2001-05-03	Changement de la structure des points fixes	barras
2001-04-24	interdiction occ positives ET negatives dans Pattern	werner
2001-04-23	reduction des let in dans whd_programs	filliatr
2001-04-20	un typage sûr pour Goal et Check	filliatr
2001-04-15	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-11	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...	filliatr
2001-04-10	réparation Correctness; options Extraction (changement de syntaxe)	filliatr
2001-04-02	mise a jour pour ocamlweb	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-15	entetes	filliatr
2001-03-14	Prise en compte des Let dans l'instance des evars	herbelin
2001-03-12	Amélioration message d'erreur conditions de garde	herbelin
2001-03-11	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin
2001-03-08	corrections de bug de la reduction	barras
2001-03-08	compare_constr independent du groupement des applications.	barras
2001-03-06	réparation (?) discharge axiome	filliatr
2001-03-05	Re-Déplacement extended_rel_list	herbelin
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-28	retire profile	mohring
2001-02-28	Changement de subst_meta	mohring
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-08	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr
2001-02-07	Chgt signature de type_of_existential	herbelin
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-01-31	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-27	make doc	herbelin
2001-01-27	Ajout alias mutual_inductive_path = section_path	herbelin
2001-01-24	Ajout global_vars_decl	herbelin
2001-01-24	Doc	herbelin
2000-12-26	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin
2000-12-25	Alias variable_path	herbelin
2000-12-20	Bug mauvais environnement dans le test d'eta-conversion	herbelin
2000-12-18	Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name	herbelin
2000-12-15	Le bon choix, c'est finalement identifier = string	herbelin
2000-12-15	Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...	herbelin
2000-12-15	- suppression mind_extract_params	filliatr
2000-12-15	Petite réorganisation	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin