coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	This will allow to merge back `Names` with `API.Names`
*	Add native compute profiling, BZ#5170	Paul Steckler	2017-08-17
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	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.
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Fix for #3154: use CUnix.sys_command to call native compiler.	Maxime Dénès	2014-12-16
\| \| \| \| \|	Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra care with cmd.exe vs sh is no longer required.
*	Fix native_compute for systems with a limited size for the command line.	Guillaume Melquiond	2014-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The call to the native compiler can fail due to the sheer amounts of -I options passed to it. Indeed, it is easy to get the command line to exceed 512KB, thus causing various operating systems to reject it. This commit avoids the issue by only passing the -I options that matter for the currently compiled code. Note that, in the worst case, this commit is still not sufficient on Windows (32KB max), but this worst case should be rather uncommon and thus can be ignored for now. For the record, the command-line size mandated by Posix is 4KB.
*	Native compiler: hide compiled files in a .coq-native subdirectory.	Maxime Dénès	2014-04-29
\|
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
	native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7