coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \|	Coq_makefile: code cleanup (less long lines, etc)	Pierre Letouzey	2016-06-07
\| \| \|
* \| \|	coq_makefile: List.iteri is now standard since OCaml 4.00	Pierre Letouzey	2016-06-07
\| \| \|
* \| \|	coq_makefile : short display of commands executed by make	Pierre Letouzey	2016-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This purely cosmetic effect is obtained by the same variables $(SHOW) and $(HIDE) as in the main Makefile of Coq. If you prefer the earlier raw output : make VERBOSE=1
* \| \|	coq_makefile: add some -ml-synonym to the ocamldep rules	Pierre Letouzey	2016-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled correctly.
\| \| *	LtacProf for Coq trunk	Jason Gross	2016-06-05
\| \|/ \|/\| \| \| \| \| \| \| \| \|	This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\\|
\| *	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
\| \|
* \|	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Tentative fix for bug #4522: Incorrect "Warning..." on windows.	Pierre-Marie Pédrot	2016-01-24
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	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
\|