coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	Prise en compte des noms longs dans les Hints et les Coercions, et ↵	herbelin	2001-01-24
\| \| \| \| \| \|	réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de constantes locales dans les Records	herbelin	2001-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1266 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Découpage des différentes fonctionnalités de build_mutual et ↵	herbelin	2000-12-19
\| \| \| \| \| \|	definition_structure + export des sous-fonctions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1155 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
*	Ajout de Record	herbelin	2000-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@275 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- global_reference traite des variables	filliatr	1999-12-03
\| \| \| \| \| \| \| \| \|	- construct_reference, avec environnement en argument - link de Class - Definition et Check au toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@193 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Version initiale	herbelin	1999-12-02
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@191 85f007b7-540e-0410-9357-904b9bb8a0f7