coq - The formal proof system

Age	Commit message (Expand)	Author
2001-03-14	interface du extract_rec. Extract_constr prend un environnement	letouzey
2001-03-14	* empty log message *	herbelin
2001-03-14	Ajout syntaxe zarith	herbelin
2001-03-14	MAJ	herbelin
2001-03-13	passage ocaml 3.01	filliatr
2001-03-13	signatures dans le bon ordre	filliatr
2001-03-13	Finite	filliatr
2001-03-13	simplification: plus de contexte pour extract_type et contexte simplifié pou...	filliatr
2001-03-13	suite de la verification des assert false	letouzey
2001-03-12	Amélioration message d'erreur conditions de garde	herbelin
2001-03-12	MAJ	herbelin
2001-03-12	Ajout list_map3	herbelin
2001-03-12	Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias dé...	herbelin
2001-03-12	fin du letin	letouzey
2001-03-12	debut let in	filliatr
2001-03-12	mise a jour commentaires'	filliatr
2001-03-12	Commentaires. Verification des assert false. Probleme des types ML arity.	letouzey
2001-03-11	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin
2001-03-11	Avancée vers la prise compte des alias dépendants; prise en compte des clau...	herbelin
2001-03-11	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin
2001-03-09	Mise a jour	mohring
2001-03-09	bug de refine: uncaught exception Array.sub	barras
2001-03-09	protection contre certaines exceptions levees par marshal_{in,out}	barras
2001-03-09	* empty log message *	mohring
2001-03-09	Ajout d'un fichier license	mohring
2001-03-09	Mise a jour credits pour la V7	mohring
2001-03-08	corrections de bug de la reduction	barras
2001-03-08	compare_constr independent du groupement des applications.	barras
2001-03-08	changement comparaison etats	filliatr
2001-03-07	distinction contexte et signature	filliatr
2001-03-06	plus de commentaires	letouzey
2001-03-06	on gele apres un Require => meilleures performances memoire, en particulier p...	filliatr
2001-03-06	réparation (?) discharge axiome	filliatr
2001-03-06	Modification de e_give_exact pour eviter d'echouer sur l'unification	mohring
2001-03-06	eta-expansion	mohring
2001-03-06	EAutod (debug)	filliatr
2001-03-06	modifs pour extraction; bug coqmktop	filliatr
2001-03-05	ocamlweb	filliatr
2001-03-05	extraction termes (suite)	filliatr
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
2001-03-05	indentation code	filliatr
2001-03-05	Re-Déplacement extended_rel_list	herbelin
2001-03-05	Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...	herbelin
2001-03-01	De bizarres SR_pus_assoc au lieu de SR_plus_assoc	herbelin
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	Inversion termast/astterm; suppression camldebug pour coqmktop -opt	herbelin
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-28	introduction d'un refine avec resolution des types et de l'instantiation des ...	mohring