coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	- condition de garde (suite)	barras	2001-12-10
\| \| \| \| \| \| \|	- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 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
*	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
*	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
*	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
*	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
*	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
*	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
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug Reset et Sections	filliatr	2001-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1410 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 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
*	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
*	Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique ↵	herbelin	2000-11-20
\| \| \| \| \| \|	export_objet aussi aux sections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵	herbelin	2000-11-06
\| \| \| \| \| \|	DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 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
*	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
*	debug reset	filliatr	1999-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 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
*	deplacement de Discharge dans toplevel	filliatr	1999-12-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add_leaf -> application methode cache	filliatr	1999-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs pour premiere edition de liens	filliatr	1999-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	portage Astterm (partiellement)	filliatr	1999-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	with_heavy_rollback deplace dans States	filliatr	1999-09-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@89 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
*	module Library	filliatr	1999-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modules System, Lib et States	filliatr	1999-09-10
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7