coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	Meilleur anglais (cf #841)	herbelin	2004-09-08
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...	herbelin	2004-08-26
*	Précisions message d'erreur	herbelin	2004-08-23
*	Distinction location ocaml 3.08 ou pas (suite)	herbelin	2004-07-29
*	Distinction location ocaml 3.08 ou pas	herbelin	2004-07-29
*	Bug tactique fix	herbelin	2004-07-28
*	"Print Setoids" command added.	sacerdot	2004-07-23
*	Abstraction vis à vis de dummy_loc	herbelin	2004-07-20
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
*	Suppression quotify	herbelin	2004-07-16
*	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