coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	Meilleur traitement des noms explicites dans la Nametab; Différentation du ↵	herbelin	2001-02-05
\| \| \| \| \| \|	traitement des sections et des modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1328 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test pour empêcher 2 sections de même noms	herbelin	2000-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 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
*	Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de ↵	herbelin	2000-12-05
\| \| \| \| \| \|	la section; 2 racines officielles pour l'espace des noms : Coq et Scratch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1047 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Enregistrement des racines de la bibliothèque	herbelin	2000-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage	herbelin	2000-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@967 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
*	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
*	implicites manuels	filliatr	2000-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle structure arborescente à la Nametab pour prendre en compte les ↵	herbelin	2000-11-20
\| \| \| \| \| \|	noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@866 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
*	- 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