coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	maj	filliatr	2003-11-05
*	En v8, une notation, c'est 2 regles et un niveau	herbelin	2003-11-04
*	Amelioration message d'erreur	herbelin	2003-11-04
*	* empty log message *	barras	2003-11-04
*	Explicitation message d'erreur nombres negatifs	herbelin	2003-11-04
*	Pour eviter des anomalies au lieu d'erreur en mode traducteur	herbelin	2003-11-04
*	Extension de zarith	herbelin	2003-11-04
*	Amelioration message d'erreur pour ltac	herbelin	2003-11-04
*	Amelioration message d'erreur avec pretyping; prise en compte syntactic def d...	herbelin	2003-11-04
*	pour que make clean efface ide/utf8_convert.ml venant d'un .mll	letouzey	2003-11-04
*	Check en plus parmi les keywords	letouzey	2003-11-03
*	Exporting ^; utilisation arg scope implicite	herbelin	2003-11-03
*	Compatibilite V7.4 pour le delimiteur de positive	herbelin	2003-11-03
*	maj	filliatr	2003-11-03
*	Cosmetique	herbelin	2003-11-02
*	Renforcement significatif du resultat principal	herbelin	2003-11-02
*	Rien de bien important	herbelin	2003-11-02
*	Commentaires	herbelin	2003-11-02
*	MAJ	herbelin	2003-11-02
*	Le printeur de Show Script n'etait pas le bon en v7	herbelin	2003-11-02
*	Typo	herbelin	2003-11-02
*	Ajout Diaconescu.v	herbelin	2003-11-02
*	AC + EXT -> EM	herbelin	2003-11-02
*	Relations entre le choix (forme relationnelle) avec restriction ou non	herbelin	2003-11-02
*	Renommage bool en boolP pour eviter la qualification	herbelin	2003-11-02
*	Restauration preference Rge a Rle pour compatibilite...	herbelin	2003-11-02
*	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin	2003-11-02
*	Protection contre les buts sans inegalite	herbelin	2003-11-02
*	Ajout CPatNotation, PrintVisibility	herbelin	2003-11-01
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Renommage Topconstr.map_aconstr_with_binders_loc	herbelin	2003-11-01
*	Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8	herbelin	2003-11-01
*	Il ne faut pas mettre le constrarg des tactiques au niveau lconstr	herbelin	2003-11-01
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Traduction des noms pour les refs de pr_glob_generic (via pr_global)	herbelin	2003-11-01
*	Utilisation de niveaux pour l'extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Extension de get_constr_entry et symbol_of_production pour gerer les extensio...	herbelin	2003-11-01
*	Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...	herbelin	2003-11-01
*	Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc	herbelin	2003-11-01
*	Ajout CPatNotation; renommage map_aconstr_with_binders_loc	herbelin	2003-11-01
*	Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter que	herbelin	2003-11-01
*	Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...	herbelin	2003-11-01
*	Interdiction de nommer un object de nom commencant par Coq en dehors de la bi...	herbelin	2003-11-01
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Heritage des notations v7 seulement si zero information v8	herbelin	2003-11-01
*	Debranchement de Print si pas verbose (necessaire pour traducteur)	herbelin	2003-11-01
*	maj	filliatr	2003-10-31
*	Redirected some of the verbose jprover output through the Pp module.	corbinea	2003-10-30
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30