coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| \|
* \|	Merge PR#843: closing bug #5618 introduce by PR 828	Maxime Dénès	2017-06-30
\|\ \
\| * \|	closing bug #5618 introduce by PR 828	Julien Forest	2017-06-29
\| \| \|
* \| \|	Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵	Maxime Dénès	2017-06-27
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	with make -j4
* \ \ \	Merge PR#826: Put plugin exports in the right compatibility file	Maxime Dénès	2017-06-26
\|\ \ \ \
* \ \ \ \	Merge PR#828: closing bug #4250	Maxime Dénès	2017-06-26
\|\ \ \ \ \ \| \| \|_\|/ / \| \|/\| \| \|
* \| \| \| \|	Merge PR#794: Cleanup of ltac cmxs	Maxime Dénès	2017-06-23
\|\ \ \ \ \
\| \| * \| \| \|	closing bug #4250	Julien Forest	2017-06-23
\| \|/ / / / \|/\| \| \| \|
\| \| \| \| *	Add tests for handling of warnings	Tej Chajed	2017-06-23
\| \| \| \| \|
\| \| * \| \|	Add test-suite file for funind, extraction with compat 8.6	Jason Gross	2017-06-22
\| \|/ / / \|/\| \| \|
\| \| * \|	Should fix a false negative reported by deps-order.sh.	Hugo Herbelin	2017-06-21
\| \|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
* \| \|	Merge PR#807: romega: fix a slowdown	Maxime Dénès	2017-06-20
\|\ \ \
* \ \ \	Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological	Maxime Dénès	2017-06-19
\|\ \ \ \
* \ \ \ \	Merge PR#760: Fixing base_include after loc is an option + a better test ↵	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	that #use"include" works
* \ \ \ \ \	Merge PR#613: Cumulativity for inductive types	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Test case for bug 5578.	Maxime Dénès	2017-06-19
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP.
* \| \| \| \| \| \|	Increase the time limit on 4366.v to make gitlab work better.	Gaëtan Gilbert	2017-06-16
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| * \| \| \| \|	Fix a bug in cumulativity	Amin Timany	2017-06-16
\| \| \| \| \| \|
\| * \| \| \| \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\| \| \| \| \| \|
\| * \| \| \| \|	Move (part of) tests from checker to success	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Due to some unknown problem coqchk fails on some inductive types when it is compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis tests.
\| * \| \| \| \|	Checker add test for non-trivial constraints	Amin Timany	2017-06-16
\| \| \| \| \| \|
\| * \| \| \| \|	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
\| * \| \| \| \|	Correct coqchk reduction	Amin Timany	2017-06-16
\| \| \| \| \| \|
\| * \| \| \| \|	Disable debug printing	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix a mistake in record declaration
\| * \| \| \| \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\| \| \| \| \| \|
\| * \| \| \| \|	Fix bugs	Amin Timany	2017-06-16
\|/ / / / /
\| \| \| \| *	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \| \| \| \|\
\| \| \| \| * \	Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints	Maxime Dénès	2017-06-15
\| \| \| \| \|\ \
\| \| \| \| * \ \	Merge PR#752: Adding a test case as requested in bug 5205.	Maxime Dénès	2017-06-15
\| \| \| \| \|\ \ \
\| \| \| \| * \ \ \	Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports	Maxime Dénès	2017-06-15
\| \| \| \| \|\ \ \ \
* \| \| \| \| \ \ \ \	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
* \| \| \| \| \| \| \| \| \|	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \|	Remove dependency on -compat flag in coq_makefile test suite.	Maxime Dénès	2017-06-15
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \|	[typeclasses eauto] Fix bug #3943: non-termination in topological	Matthieu Sozeau	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	sorting for the dependency order option.
* \| \| \| \| \| \| \| \| \| \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
\| \| \| * \| \| \| \| \| \| \|	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
\| \| * \| \| \| \| \| \| \|	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#498: Bignums as a separate opam package	Maxime Dénès	2017-06-14
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#385: Equality of sigma types	Maxime Dénès	2017-06-13
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#757: Better sectioning on travis log printing in test-suite	Maxime Dénès	2017-06-13
\|\ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \|	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* \| \| \| \| \| \| \| \| \|	Merge PR#709: Bytecode compilation apart from 'make world', again	Maxime Dénès	2017-06-12
\|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \|	Add support for "-bypass-API" argument of "coq_makefile"	Matej Košík	2017-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
* \| \| \| \| \| \| \| \| \| \|	make test-suite/save-logs.sh usable also on old MacOS X	Maxime Denes	2017-06-12
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \|	A stronger test that #use"include";; works well.	Hugo Herbelin	2017-06-11
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	Fix Travis sectioning	Jason Gross	2017-06-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right?