coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement et export de type_of_global dans Global	herbelin	2001-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2178 85f007b7-540e-0410-9357-904b9bb8a0f7
*	corrections mineures suite au commit de restructuration du noyau	barras	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey	2001-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Patch de goption.ml pour faire marcher les options synchrones. Passage des ↵	letouzey	2001-10-24
\| \| \| \| \| \|	options d'extraction en synchrone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2137 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
*	Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵	herbelin	2001-10-12
\| \| \| \| \| \|	grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 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
*	Réparation des options Set Printing and co	herbelin	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre des arguments farfelus pour les implicites manuels	herbelin	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2045 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make doc	filliatr	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparent	barras	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage des commentaires	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage des commentaires	herbelin	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 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
*	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵	herbelin	2001-09-19
\| \| \| \| \| \|	des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 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
*	Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵	herbelin	2001-09-19
\| \| \| \| \| \|	le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 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
*	Mise en place de noms contenant la section pour Fact et Remark	herbelin	2001-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1987 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
*	Transformation de Remark/Fact en constantes non visibles sans qualification	herbelin	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1969 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵	herbelin	2001-09-10
\| \| \| \| \| \|	éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Légère modification lookup_eliminator	herbelin	2001-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1943 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mécanisme pour faire remonter les contraintes de typage sur les variables ↵	herbelin	2001-09-09
\| \| \| \| \| \|	de section au niveau du discharge, sans avoir à garder tout l'environnement de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 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
*	Rétablissement de Print Section	herbelin	2001-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1926 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug default module name (2eme)	herbelin	2001-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug default module name	herbelin	2001-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1923 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hack rapide pour réduire significativement la taille des vo	herbelin	2001-08-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1893 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
*	Ajout error_global_not_found	herbelin	2001-08-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout make_elimination_ident	herbelin	2001-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1869 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
*	Interdiction de faire 2 variables de même nom court	herbelin	2001-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1828 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bug Omega	filliatr	2001-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
\| \| \| \| \| \| \|	ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un commentaire erroné.	clrenard	2001-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	construct_reference regarde d'abord dans le contexte local, puis les globaux	filliatr	2001-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1743 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
*	Changement de la structure des points fixes	barras	2001-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7