coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	More substance on discouraged practices.	Théo Zimmermann	2017-06-29
\|
*	Some more corrections to the tutorial.	Théo Zimmermann	2017-06-29
\|
*	Mask the reliance on coqtop.	Théo Zimmermann	2017-06-29
\|
*	Update the Tutorial.	Théo Zimmermann	2017-06-28
\|
*	Merge PR#825: Ignore all PDF files.	Maxime Dénès	2017-06-26
\|\
* \	Merge PR#828: closing bug #4250	Maxime Dénès	2017-06-26
\|\ \
* \ \	Merge PR#824: Fix printers	Maxime Dénès	2017-06-23
\|\ \ \
* \ \ \	Merge PR#821: [vernac] Remove stale bool parameter from ↵	Maxime Dénès	2017-06-23
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`VernacStartTheoremProof`
* \ \ \ \	Merge PR#820: [ide] Correct more merging errors.	Maxime Dénès	2017-06-23
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#815: STM: par: report no error to UIs in non-solve mode	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#794: Cleanup of ltac cmxs	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#762: [vernac] Fix unneeded mutual references in Obligations	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \|	closing bug #4250	Julien Forest	2017-06-23
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Ignore all PDF files.	Théo Zimmermann	2017-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Rules for ignoring some PDF files had been added one by one to `.gitignore` but some were still missing (for the corresponding latex files in `dev`). This rule is actually better since we are not tracking any PDF file.
* \| \| \| \| \| \| \|	Merge PR#817: [stm] Fix route setting on VtQuery	Maxime Dénès	2017-06-22
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Add missing definition and fix #use include;; as suggested by @amintimany.	Théo Zimmermann	2017-06-22
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	[vernac] Remove stale bool parameter from `VernacStartTheoremProof`	Emilio Jesus Gallego Arias	2017-06-21
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
\| \| \| \| \| *	[ide] Correct more merging errors.	Emilio Jesus Gallego Arias	2017-06-21
\| \|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	This file doesn't want to leave us.
\| * \| \| \|	[stm] Fix route setting on VtQuery	Emilio Jesus Gallego Arias	2017-06-20
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter.
\| \| \| *	STM: par: report no error to UIs in non-solve mode	Enrico Tassi	2017-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve")
\| * \| \|	[vernac] Remove forward hooks from Obligations.	Emilio Jesus Gallego Arias	2017-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.
\| * \| \|	[vernac] Remove unused hooks.	Emilio Jesus Gallego Arias	2017-06-20
\|/ / / \| \| \| \| \| \| \| \| \|	These hooks are not used (leftovers?) and IMHO they should not be.
* \| \|	Merge PR#742: Fix `make TIMED=1` garbage	Maxime Dénès	2017-06-20
\|\ \ \
* \ \ \	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\ \ \ \
* \ \ \ \	Merge PR#793: Fixing restriction of existential variables regarding evar_store	Maxime Dénès	2017-06-20
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#807: romega: fix a slowdown	Maxime Dénès	2017-06-20
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#803: Clean ssr	Maxime Dénès	2017-06-20
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#790: Direct link to Travis branch builds.	Maxime Dénès	2017-06-20
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#779: Each user overlay goes into its own file.	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#777: Improving documentation of tactic "move" (report #4561)	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#795: [ide] Better exn printing. [fixes BZ#5524]	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#727: [tactics] Fix summary registration of global hint variable.	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix typo in comment.	Maxime Dénès	2017-06-19
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#784: API additions for coq-dpdgraph	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#755: "There are pending proofs" error message now lists the name of ↵	Maxime Dénès	2017-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the proofs.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[ide] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[ide] Better exn printing. [fixes BZ#5524]	Emilio Jesus Gallego Arias	2017-06-18
\| \| \| \| \| \| \|_\|_\|_\|_\|_\|_\|_\|/ / / \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.	Maxime Dénès	2017-06-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	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.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#759: don't leak unqualified identifiers from the macro	Maxime Dénès	2017-06-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Add coq-dpdgraph to gitlab CI	Gaëtan Gilbert	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	"There are pending proofs" error message now lists the name of the proofs.	Théo Zimmermann	2017-06-16
\| \|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This closes https://coq.inria.fr/bugs/show_bug.cgi?id=5275
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Increase the time limit on 4366.v to make gitlab work better.	Gaëtan Gilbert	2017-06-16
\| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Each user overlay goes into its own file.	Théo Zimmermann	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will avoid stupid merge conflicts in the future.
\| \| \| \| \| \| \| \| \| \| * \| \| \|	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
\| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove the last use of the low-level Proof_type API in ssr.	Pierre-Marie Pédrot	2017-06-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|