coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
\| \| \| \| \| \| \|	et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des ↵	herbelin	2005-12-26
\| \| \| \| \| \|	G_new en G_.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement des named_context	gregoire	2005-12-02
\| \| \| \| \| \| \| \|	Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	Licence changed from GPL to Lesser GPL.	sacerdot	2004-06-26
\| \| \| \| \| \| \|	DTDs licence is still GPL. This should create no problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5828 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Copyright notice of files in contrib/xml made uniform.	sacerdot	2004-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Loic code to pretty-print the generated proof-tree debranched (since it	sacerdot	2004-04-07
\| \| \| \| \| \| \| \|	generates not well-formed XML files). An hook is left in xmlcommand.ml to register a pretty-printer function once a fixed implementation is provided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ProofTree2Xml is no longer directly used by Xmlcommand.	sacerdot	2004-03-25
\| \| \| \| \| \| \| \|	On the contrary, it registers itself using the hook provided by Xmlcommand. The obtained design is more modular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5563 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation du printer approprie a la version de syntaxe	herbelin	2004-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration de la branche mowgli	herbelin	2002-11-05
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3213 85f007b7-540e-0410-9357-904b9bb8a0f7