coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-of-the-box.	gmelquio	2009-09-28
\| \| \| \| \| \| \|	- Removed unneeded bashisms. (sh and dash are fine with the current build system.) - Removed workaround for camlp4.opt on BSD. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branch	herbelin	2009-04-08
\| \| \| \| \| \| \| \| \| \|	(r12063) for smooth compilation/installation under Solaris (/bin/sh -> /bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than in if). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: fix ignored errors, several attempts to clarify things	letouzey	2009-03-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* I encountered error messages during compilation, for instance ocamlopt complaining about non-existing coq_config.cmi when compiling coq_config.ml. Moreover, make was _not_ stopping at these errors (WTF?!). After some debug, it turned out to be (indirectly) my fault: I placed earlier the inclusion of the new .mllib.d in Makefile.stage1, but this is too early, coqdep, which is used to compute these files, isn't built yet. Due to the semantics of "-include", make tries to build it, fails with the above error, and goes on happily. Arrgh. After moving the inclusion of these .mllib.d to Makefile.stage2, everything seems to work ok now. * Since we're using such "nice" non-trivial features of make, I've started a small FAQ section about them at the beginning of Makefile * Recursive calls to make are now done with two options: --no-builtin-rules : let's avoid builtin rules like "%:%.o" ... --warn-undefined-variable : using a non-defined variable isn't necessarily bad, but I found a few bugs with this option, and I suggest we keep it. * Clarified the rules about stage* in Makefile and their STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_ have a chance to grasp in less than a day what's going on ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: ml dependencies of contribs are moved to .mllib files	letouzey	2009-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 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
*	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