coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin	2004-03-02
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin	2004-03-02
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
*	added breakpoints to help ide	corbinea	2004-02-26
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	bugs avec Pose et Assert	barras	2004-01-09
*	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin	2003-12-19
*	Amélioration du message d'erreur "w_unify"	clrenard	2003-12-01
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Amelioration du message d'erreur en cas de tentative d'instanciation	clrenard	2003-11-15
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
*	Ajout pf_apply	herbelin	2003-11-09
*	Added Instantiate ... in	corbinea	2003-11-06
*	2 espaces en trop	herbelin	2003-11-05
*	Amelioration de l'afficheur de script structure	herbelin	2003-11-05
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	code mort	herbelin	2003-10-10
*	pf_get_new_id en provenance de feu wcclausenv	herbelin	2003-10-10
*	Suppression clenv_change_head que seul Wcclausenv utisait	herbelin	2003-10-10
*	Cablage en dur de inversion	herbelin	2003-10-10
*	Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin	2003-09-12
*	open superflu	herbelin	2003-09-12
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	Ground update	corbinea	2003-07-08
*	Ground Update.	corbinea	2003-06-20
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin	2003-06-10
*	Ajout FreshId	herbelin	2003-05-24
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	coqide: toolbar/autosave	monate	2003-05-07
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
*	Localisation des appels de tactiques définies sans arguments	herbelin	2003-04-14
*	Affichage des tactiques en v8	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Réparation bug de l'unification. En effet, avant l'instanciation d'une evar	clrenard	2003-03-28
*	* empty log message *	barras	2003-03-12
*	Debugger plus informatif	delahaye	2003-02-13
*	Bug Rename	herbelin	2003-02-08
*	Pour satisfaire ProofGeneral	coq	2003-01-31