coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans ↵	herbelin	2004-03-28
\| \| \| \| \| \|	coqtop.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5592 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2003-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	id_of_msid en plus	letouzey	2003-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrections de gestion des univers et modules + meilleure gestions des ↵	coq	2002-12-09
\| \| \| \| \| \|	noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	des Set et des Map en plus	letouzey	2002-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3379 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrige un bug de composition de substitutions	coq	2002-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3372 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hash-consing pour kernel_name	herbelin	2002-09-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3048 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
\| \| \| \| \| \| \| \| \| \| \| \| \|	Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation de Locate	barras	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 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
*	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 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
*	Transparent	barras	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Romega	mohring	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des dir_path vide	herbelin	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Romega/names/Makefile	mohring	2001-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras	2001-09-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1920 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 add_prefix/add_suffix	herbelin	2001-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1868 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
*	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
*	Mise en place d'un système optionnel de discharge immédiat; prise en ↵	herbelin	2001-02-14
\| \| \| \| \| \|	compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'espace dans les règles d'affichage des infix si des lettres ↵	herbelin	2001-01-31
\| \| \| \| \| \|	figurent dans le token git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout alias mutual_inductive_path = section_path	herbelin	2001-01-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1282 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Alias variable_path	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Le bon choix, c'est finalement identifier = string	herbelin	2000-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un module Ident avec test de l'efficacité quand ↵	herbelin	2000-12-15
\| \| \| \| \| \|	identifier=string git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1130 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mini-nettoyage noms longs	herbelin	2000-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un test pour vérifier qu'on a affaire à un ident	herbelin	2000-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1012 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
*	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
*	Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp	herbelin	2000-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@929 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵	herbelin	2000-11-22
\| \| \| \| \| \|	'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Introduction constant_path = section_path	herbelin	2000-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug sur précédent commit	herbelin	2000-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage Names suite	herbelin	2000-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@818 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
*	bug make_strength repare	filliatr	1999-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@200 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
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	diverses fonctions ajoutees	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@170 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- un effort sur la doc (ocamlweb)	filliatr	1999-09-19
\| \| \| \| \| \| \| \| \|	- module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 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