coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	GROS COMMIT:	barras	2001-11-05
\| \| \| \| \| \| \| \| \| \|	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵	herbelin	2001-10-17
\| \| \| \| \| \|	sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	One more boolean test bug	herbelin	2001-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2057 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug test booléen	herbelin	2001-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nombre magique pour la V7.1	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas de warning pour le -I . par défaut de Coq	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2023 85f007b7-540e-0410-9357-904b9bb8a0f7
*	warning silencieux	filliatr	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restriction de l'avertissement add_loadpath au mode verbeux	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2017 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Autorisation de surcharge d'un -R par un -I	herbelin	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1990 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative de canonisation des répertoires physiques	herbelin	2001-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques heuristiques pour gérer des représentations similaires de paths ↵	herbelin	2001-09-18
\| \| \| \| \| \|	syntaxiquement différents git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1985 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des library roots, on teste si un nom est absolu autrement	herbelin	2001-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1927 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parsing	herbelin	2001-08-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur le warning Require en Section: trop contraignant	herbelin	2001-07-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1834 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avertissement contre les Require dans le corps d'une section	herbelin	2001-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1829 85f007b7-540e-0410-9357-904b9bb8a0f7
*	quelques bug reports mineurs	barras	2001-05-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1733 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	protection contre certaines exceptions levees par marshal_{in,out}	barras	2001-03-09
\| \| \| \| \| \| \|	possibilite de declarer une def syntaxique comme infix (utilise par FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	on gele apres un Require => meilleures performances memoire, en particulier ↵	filliatr	2001-03-06
\| \| \| \| \| \|	pour Proof General git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification du make depend; fonctions de stat. util. memoire dans ↵	filliatr	2001-02-08
\| \| \| \| \| \|	certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin	2001-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Import module force l'ouverture du module même s'il était déjà ouvert ↵	herbelin	2000-12-20
\| \| \| \| \| \|	afin de pouvoir re-rendre visible des noms ayant été cachés depuis l'ouverture du module; renommage de open_module en import_module avec cette nouvelle spéc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1164 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation de bugs de LoadPath	herbelin	2000-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1123 85f007b7-540e-0410-9357-904b9bb8a0f7
*	load_path_entry structure simplified; field relative_subdir renamed to coq_dirpa	sacerdot	2000-11-29
\| \| \| \| \| \| \|	th; add_path now checks for directory existence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ↵	herbelin	2000-11-29
\| \| \| \| \| \|	chemin Unix à un chemin Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte du repertoire dans le section path; utilisation de dirpath ↵	herbelin	2000-11-28
\| \| \| \| \| \|	pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	load_module / open_module un tantinet plus rapides	filliatr	2000-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de noms absolus dans la nametab	herbelin	2000-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr	2000-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
*	certains effets disparaissent a la sortie des sections, d'autres non (selon ↵	filliatr	2000-11-24
\| \| \| \| \| \|	Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
*	synchronisation Require	filliatr	2000-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@941 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement poly_args; iterateurs sur les segments	filliatr	2000-11-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Open est maintenant géré par Nametab	herbelin	2000-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@869 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵	herbelin	2000-11-10
\| \| \| \| \| \|	library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@841 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau load path	filliatr	2000-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
*	out_variable (Liboject.obj -> ...) distibgue de get_variable	filliatr	2000-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@821 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- simplification Makefile (compilation des fichiers .ml'; pas encore parfait	filliatr	2000-10-31
\| \| \| \| \| \| \| \|	car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour le Require Export (temporaire)	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@784 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Require Export recursifs	filliatr	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module_segment et module_filename	filliatr	2000-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. ↵	herbelin	2000-09-10
\| \| \| \| \| \|	Abstraction de constr. LetIn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@589 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
\| \| \| \| \| \| \| \| \| \|	- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modules	filliatr	1999-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- constantes avec recettes	filliatr	1999-12-09
\| \| \| \| \| \| \| \|	- discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modules Bij, Gmapl, Stock	filliatr	1999-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@125 85f007b7-540e-0410-9357-904b9bb8a0f7
*	juste l'interface de Discharge	filliatr	1999-09-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@85 85f007b7-540e-0410-9357-904b9bb8a0f7
*	module Declare	filliatr	1999-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7