coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouvelle en-tête	herbelin	2004-07-16
*	Branchement sur Util.loc et abstraction vis a vis de dummy_loc	herbelin	2004-07-16
*	Abstraction vis a vis de dummy_loc	herbelin	2004-07-16
*	bugs #667 and #783 (mimick_evar and loc_table on large files)	barras	2004-07-13
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	efficacite du lexeur	filliatr	2004-06-29
*	more evar stuff	corbinea	2004-06-28
*	Nouvelle syntaxe à la ML pour donner le type ML des extensions d'arguments	herbelin	2004-06-17
*	Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)	herbelin	2004-06-03
*	Affichage de l'opacité dans Print et About	herbelin	2004-06-02
*	Bug affichage ClearBody	herbelin	2004-05-27
*	Bug syntaxe AddPath	herbelin	2004-05-14
*	Ajout entree pour exporter les commentaires en mode -xml	herbelin	2004-03-26
*	Code mort	herbelin	2004-03-25
*	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin	2004-03-17
*	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin	2004-03-17
*	Parsing des V8Notation avec motif recursif en v7	herbelin	2004-03-17
*	Utilisation de '..' pour la notation concrete des motifs recursifs de filtrage	herbelin	2004-03-17
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin	2004-03-03
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	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
*	Correction oubli du cas pas d'arguments implicites du tout	herbelin	2004-03-02
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin	2004-03-01
*	Expansion du type par nécessité dans le cas d'affichage d'implicites	herbelin	2004-02-28
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...	herbelin	2004-02-21
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin	2004-02-17
*	export the general function for getting information from the environment	bertot	2004-02-16
*	Uniformisation du comportement de Notation et Reserved Notation	herbelin	2004-02-13
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	Suppression de 'Print.' en v8	herbelin	2004-01-29
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin	2004-01-29
*	Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...	herbelin	2004-01-27
*	reparation de qqs bugs du traducteur	barras	2004-01-26
*	Protection table des locations lors de Load (pour coqdoc)	herbelin	2004-01-22
*	Export information des references et location de notations pour coqdoc	herbelin	2004-01-21
*	Le traducteur utilisait un afficheur des reels obsolete et bugge	herbelin	2004-01-20
*	Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8	herbelin	2004-01-20
*	make libraries, lexing of more utf8 symbols	marche	2004-01-14
*	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin	2004-01-13
*	Reference obsolete au niveau 200 de pattern	herbelin	2004-01-13
*	bugs avec Pose et Assert	barras	2004-01-09
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Bug affichage Decompose	herbelin	2003-12-24
*	* empty log message *	barras	2003-12-23
*	Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...	herbelin	2003-12-22