coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896).	Guillaume Melquiond	2016-07-05
\| \| \| \| \|	Coqc now expects physical names for input files, so fix coq_makefile accordingly.
*	Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).	Guillaume Melquiond	2016-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The COQLIBS variable contains some -Q and -I options, which are not supported by the checker. So this commit introduces a COQCHKLIBS variable that contains the proper options for coqchk. For the sake of homogeneity, the COQDOCLIBS variable is also preprocessed in the same way. This means that both variables have the same value, but they are kept separate in case the user would like to override one and not the other. This commit also removes some deprecated options from "coqchk --help". They are not removed from coqchk itself to preserve backward compatibility in the branch. An open question is whether coqchk should support dummy options such as -Q (interpreted as -R) or -I (ignored).
*	use printf instead of sequenced calls to print.	Gregory Malecha	2016-03-24
\|
*	add a .merlin target to the makefile	Gregory Malecha	2016-03-24
\|
*	Tentative fix for bug #4522: Incorrect "Warning..." on windows.	Pierre-Marie Pédrot	2016-01-24
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)	Guillaume Melquiond	2015-09-16
\|
*	Missing argument "-c" for coqdep in coq_makefile	mlasson	2015-09-03
\| \| \| \| \| \| \| \| \|	Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d were generated by a call to coqdep using the argument -c (for ocaml code). While doing some finetuning of the generation of implicit rules, this commit removed (I think by mistake) this "-c". And without this -c argument coqdep output nothing on mllib files leading to incorrect linking of mllibs.
*	Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.	Guillaume Melquiond	2015-07-30
\| \| \| \| \| \| \| \|	"This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
*	Do not regenerate .d files when cleaning them. (Fix bug #4079)	Guillaume Melquiond	2015-05-14
\|
*	Remove some spurious spaces in generated Makefiles.	Guillaume Melquiond	2015-04-22
\|
*	coq_makefile: fix compilation with camlp4	Enrico Tassi	2015-03-30
\|
*	Properly handle extra "clean" targets with coq_makefile.	Guillaume Melquiond	2015-03-27
\|
*	End of Bug 3986 - make cleanall removes .*.aux files	Pierre Boutillier	2015-03-14
\|
*	Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning	Pierre Boutillier	2015-03-14
\|
*	Coq_makefile clean target erases .coq-native dirs in . if they are empty	Pierre Boutillier	2015-02-28
\|
*	Fixing the rule for ml4 depencies in coq_makefile	mlasson	2015-02-28
\|
*	Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵	Guillaume Melquiond	2015-02-27
\| \| \| \|	bug #4080)
*	Fixing printing error in coq_makefile.	Pierre-Marie Pédrot	2015-02-26
\|
*	Mention -R option in warnings, fixing #4067 and #4068.	Maxime Dénès	2015-02-26
\|
*	Update the list of phony targets produced by coq_makefile. (Fix for bug #4084)	Guillaume Melquiond	2015-02-24
\| \| \| \|	Also make uninstall_me.sh a real target with proper dependencies.
*	Fixed a wrong warning in coq_makefile.	Pierre Courtieu	2015-01-27
\| \| \| \|	A non empty dir detected as an empty one.
*	coq_makefile: install also .v and .glob	Enrico Tassi	2015-01-16
\| \| \| \| \| \|	This is useful for PIDE based interfaces, since they can build hyperlinks out of .glob files and let the user jump to the corresponding .v files
*	Remove left-over dead code in previous commit.	Maxime Dénès	2015-01-15
\|
*	Make -print-mod-uid accept a list of files.	Maxime Dénès	2015-01-15
\| \| \| \|	Solves an efficiency problem in Makefiles generated by coq_makefile.
*	Make installation of native files more robust.	Maxime Dénès	2015-01-15
\|
*	coq_makefile installs native files	Pierre Boutillier	2015-01-15
\|
*	coq_makefile: chmod 755 on toplopp cmxs	Enrico Tassi	2015-01-14
\|
*	Made -print-mod-uid more silent and robust.	Maxime Dénès	2015-01-13
\| \| \| \|	This is a follow-up on Pierre's 5d80a385.
*	Coq_makefile erases native compiler files	Pierre Boutillier	2015-01-12
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	rename: vi -> vio	Enrico Tassi	2015-01-06
\|
*	Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for ↵	mlasson	2014-12-18
\| \| \| \|	grammar in campl4
*	Fix #3800 : cmxs need execution priviledges under windows	Pierre Boutillier	2014-12-12
\|
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
\|
*	Coq_makefile: Allow empty logical names	Pierre Boutillier	2014-10-09
\| \| \| \|	I'm not sure that coqdep and coqtop understand them correctly anyway ...
*	coq_makefile: explicit target install-toploop for toploop plugins	Enrico Tassi	2014-10-07
\|
*	fix wrong escaping in coq_makefile	Enrico Tassi	2014-10-06
\|
*	coq_makefile: build and install *top.cmxs plugins	Enrico Tassi	2014-10-01
\| \| \| \| \| \| \| \|	These plugins, like coqidetop, stmworkertop and tacworkertop are intended for toploop replacements (see -toploop command line option). With this commit coq_makefile can be used as the build system for any user-interface-specific plugins.
*	fix coq_makefile	Pierre Boutillier	2014-09-18
\|
*	Coq_makefile: fix cmx compilation when there are both ml and mllib	Pierre Boutillier	2014-07-07
\|
*	Fix Coq_makefile in presence of mlpack	Pierre Boutillier	2014-07-03
\|
*	Bug 3405: Coq_makefile: Implicit rules only for listed files in Make file	Pierre Boutillier	2014-07-03
\|
*	Coq_makefile takes advantages of -I -Q -R cleanup	Pierre Boutillier	2014-06-30
\|
*	Coq_makefile: -extra[-phony] correction + doc	Pierre Boutillier	2014-06-30
\|
*	coq_makefile: -I for the new stm/ dir	Enrico Tassi	2014-04-25
\|
*	Adapt coq_makefile build rules to new -R -I semantic	Pierre Boutillier	2014-04-09
\|
*	Fix compilation of coq and plugins using coq_makefile under cygwin	Enrico Tassi	2014-02-28
\| \| \| \| \| \| \| \| \|	Problems: - strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config the value of "ranlinb" and replace ranlib by strip obtaining "i686-bla-strip" from "i686-bla-ranlib" - coq_makefile was not quoting the plugins/ paths - coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
*	coq_makefile: new target vi2vo	Enrico Tassi	2014-02-26
\|
*	-schedule-vi-checking ported to spawn	Enrico Tassi	2014-01-26
\|