coq - the Coq proof assistant

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