coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Plongement de doc/Makefile dans la nouvelle architecutre des Makefile	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implement KEEP_ML4_PREPROCESSED option in build system	lmamane	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implement NO_RECALC_DEPS option in build system	lmamane	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration de la génération des graphes de dépendances	notin	2008-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	migration of ide/utf8.v to theories/Unicode/Utf8.v	letouzey	2007-12-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These notations aren't CoqIDE-specific, I can now use them with ProofGeneral (after a small modification of PG, contact me if you're interested by the patch). So let's place this file in a globally visible subdir of theories/. By the way, the filename is now uppercase as all other .v files. By the way, minor other changes in Makefile : extraction/test doesn't exist anymore, and tags / otags can be made without re-doing any find. NB: be sure to use etags that comes from emacs and not the one of exuberant-ctags, since the latter has now a different syntax (in debian, see update-alternatives etags). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1741	notin	2007-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10314 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intallation des .cma/.cmxa	notin	2007-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10241 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Copie des .cma et des .cmxa, et de grammar.cma dans le répertoire de Coq ↵	notin	2007-10-18
\| \| \| \| \| \|	(pour faciliter la compilation des tactiques ml par les utilisateurs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Allow a few build system optimisations/corner-cutting	lmamane	2007-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Calcul des dependances sous Windows	notin	2007-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10196 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1715	notin	2007-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option -lablgtkdir au configure (basé sur patch de Guillaume	herbelin	2007-10-04
\| \| \| \| \| \| \| \|	Rousse -- rapport de bug #1713) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10176 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation sous windows	notin	2007-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10171 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preventing gcc to generate dependencies wrt OCaml files (otherwise, we run ↵	notin	2007-10-02
\| \| \| \| \| \|	into troubles under Windows) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10166 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: Revert r10015, which was based on a misunderstanding	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: needs GNU Make 3.81	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: more robustness all around	lmamane	2007-07-18
\| \| \| \| \| \| \| \|	- Make sure make notices when a command fails - don't leave behind half-baked output files of commands that failed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ↵	lmamane	2007-07-17
\| \| \| \| \| \|	anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: -MG doesn't (and can't) do what is necessary	lmamane	2007-07-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The -MG option causes gcc to add any non-found .h file verbatim in the dependencies. This naturally doesn't include the path to it (because the path is unknown) and thus make doesn't know how to build it; it knows how to build kernel/byterun/coq_jumptbl.h, not "coq_jumptbl.h". --This line, and those below, will be ignored-- M Makefile.common M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A cleaner solution to "make deletes .ml4.d files -> infinite loop" problem	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oups... empty .ml4.d files produced	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CAMLP4DEPS will not work for .byteml and .optml	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
\| \| \| \| \| \| \| \|	Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: work around gcc bug: lhs of make rule created by -MM does not ↵	lmamane	2007-07-16
\| \| \| \| \| \|	include path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: in C, .d files need to depend on the same as the .o file	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	makefile: dependencies of .c files: assume missing headers are generated files	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: use CFLAGS for dependency generation of .c files	lmamane	2007-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A emacs-specific comment to use makefile-mode on Makefile.*	letouzey	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
	Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7