coq - The formal proof system

Age	Commit message (Expand)	Author
2003-04-16	prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...	letouzey
2003-04-07	Ajout translate	herbelin
2003-04-07	Globalisation tactiques	herbelin
2003-04-07	Options d'affichage maintenant dans Constrextern	herbelin
2003-03-18	Ajout translate	herbelin
2003-03-07	Petites modifs de mes super-Makefiles ;)	coq
2003-01-19	Ajout pptac	herbelin
2002-12-05	Ajout affichage fconstr	herbelin
2002-11-24	Ajout interp	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-04	ajout d'un printer pour les global_reference	letouzey
2002-10-05	Lazy experimentale temporaire...	coq
2002-10-01	Cool dev/Makefile's	coq
2002-09-20	La notation with dependante + affichage dependante de moduels corrige	coq
2002-09-13	Ajout contribs manquantes	herbelin
2002-08-19	Pretty-printing preliminaire des modules, commandes	coq
2002-08-13	AutoRewrite substitutive...	coq
2002-08-13	Petites corrections ici et la	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-14	* empty log message *	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-02-20	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-07	suppression du retour chariot a la fin de print_pure_constr	barras
2002-01-07	MAJ	herbelin
2001-12-19	Pour les développeurs extérieurs	herbelin
2001-12-19	Réorganisation	herbelin
2001-12-19	Pour les développeurs extérieurs	herbelin
2001-12-19	MAJ V7.2	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-30	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye
2001-08-10	Parsing	herbelin
2001-06-27	correction d'un bug de Correctness (pour Y Bertot)	filliatr
2001-05-29	Retablissement de minicoq	coq
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-15	Modification pour passage p-automates	mohring
2001-05-10	ajout d'un afficher de contexte et d'une fonction constbody_of_string	letouzey
2001-05-03	Changement de la structure des points fixes	barras
2001-04-03	Make sure that the COQTOP variable is really used, when it is set.	bertot
2001-03-15	entetes	filliatr
2001-03-06	modifs pour extraction; bug coqmktop	filliatr
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
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	nouvelle implantation de la reduction	barras