coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-05	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin
2003-11-05	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin
2003-11-05	Renommage canonique d'un lemme redondant	herbelin
2003-11-05	Redondances	herbelin
2003-11-05	Modules obsoletes de ZArith en v8	herbelin
2003-11-05	Nouvelle vague de renommage	herbelin
2003-11-05	Déport des lemmes de Omega de ZArith vers OmegaLemmas	herbelin
2003-11-05	Ajout NArith et restructuration ZArith	herbelin
2003-11-05	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...	herbelin
2003-11-05	MAJ	herbelin
2003-11-05	Renommage canonique d'un lemme redondant	herbelin
2003-11-05	Branchement de Show Script sur l'afficheur structure	herbelin
2003-11-05	Amelioration de l'afficheur de script structure	herbelin
2003-11-05	maj	filliatr
2003-11-04	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-03	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-02	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-01	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