coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\
\| *	Change coq_makefile's default from "-Q . Top" to "-R . Top". (Fix bug #3603)	Guillaume Melquiond	2015-09-16
\| \|
* \|	Coq_makefile: read TIMED and TIMECMD from environment.	Maxime Dénès	2015-09-13
\| \| \| \| \| \| \| \|	Useful e.g. with submakefiles.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\|
\| *	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.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	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."
* \|	All invocations to ocaml compilers go through ocamlfind	Pierre Boutillier	2015-06-22
\| \| \| \| \| \| \| \| \| \|	Nothing is done for camlp4 There is an issue with computing camlbindir
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
\| *	Do not regenerate .d files when cleaning them. (Fix bug #4079)	Guillaume Melquiond	2015-05-14
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Remove some spurious spaces in generated Makefiles.	Guillaume Melquiond	2015-04-22
\| \|
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	coq_makefile: fix compilation with camlp4	Enrico Tassi	2015-03-30
\| \|
\| *	Properly handle extra "clean" targets with coq_makefile.	Guillaume Melquiond	2015-03-27
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	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
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	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
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-28
\|\\|
\| *	Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵	Guillaume Melquiond	2015-02-27
\| \| \| \| \| \| \| \|	bug #4080)
* \|	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot	2015-02-27
\|/ \| \| \| \| \| \|	together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.
*	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
\|