coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin	2003-12-19
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	ajout test de non-regression Clear d'une def locale	barras	2003-12-17
*	MAJ suppression 250	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	correction bug: parentheses ne cassent plus les implicites	barras	2003-12-08
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin	2003-12-04
*	Symetrisation parsing/printing 'abstract'	herbelin	2003-12-04
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	Ajout ne_string	herbelin	2003-11-27
*	Protection contre les notations vides	herbelin	2003-11-26
*	Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...	herbelin	2003-11-26
*	modif lexer: ident peut commencer par _	barras	2003-11-25
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	Prise en compte des definitions locales dans les (co-)points-fixes	herbelin	2003-11-23
*	Suppression des niveaux vides	herbelin	2003-11-21
*	Ajout Print Implicit	herbelin	2003-11-21
*	Pas d'entrees autres que les predefinies en v8	herbelin	2003-11-21
*	Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...	herbelin	2003-11-20
*	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin	2003-11-19