coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	Nouvelle en-tête	herbelin	2004-07-16
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	code mort	herbelin	2003-10-10
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	coqide: toolbar/autosave	monate	2003-05-07
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin	2002-05-29
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	compat ocaml 3.03	filliatr	2001-12-13
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Re-installation de l'affichage des globaux par des noms courts	herbelin	2001-11-19
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	Parsing	herbelin	2001-08-10
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin	2001-06-25
*	Pretty -> Prettyp	filliatr	2001-05-28
*	Ajout de _ dans les patterns d'intro	mohring	2001-04-12
*	entetes	filliatr	2001-03-15
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Ajout set_lc	herbelin	2000-12-20
*	Portage d'AutoRewrite	delahaye	2000-12-02
*	Affichage des paths avec des '.', 2eme; prise en compte qualid	herbelin	2000-11-23
*	Traitement du pretty-print des Redexp	delahaye	2000-11-21
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	Renommage canonique :	herbelin	2000-10-18
*	Rebranchement de la tactique Let	herbelin	2000-10-03
*	Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...	herbelin	2000-09-26
*	Pattern matching de sous-termes	delahaye	2000-08-17
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Completion d'un match non exhaustif	delahaye	2000-05-03
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	Renommage bdize -> ast_of_constr	herbelin	2000-04-28
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
*	Abstraction de l'implémentation des signatures de Sign en vue intégration d...	herbelin	2000-01-26
*	Renommage command en constr	herbelin	2000-01-07
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	module Pfedit	filliatr	1999-12-01
*	- environment -> safe_environment	filliatr	1999-12-01
*	- Typing -> Safe_typing	filliatr	1999-12-01
*	Backtrack sur modif Evd.evd_concl	herbelin	1999-11-25