coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|/ / / / / / \| \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Bump version number to 8.6.1.	Maxime Dénès	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fix libpcre dependency issue under Windows.	Maxime Dénès	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fix proxy setting issue	Michael Soegtrop	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fixes bug #5561,#5562 in Windows build system	Michael Soegtrop	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Merge PR#756: Fix Bug #5574, document function scope	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \	Merge PR#813: Fix plugin warnings	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix Bug #5574, document function scope	Paul Steckler	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| / \| \| \|	closing bug #4250	Julien Forest	2017-06-23
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[configure] 'ocaml' is more precise than OCaml as we mean the binary.	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix suggested by Hugo.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	ocaml -> OCaml in configure.ml.	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Merge PR#729: Fixing an inconsistency between configure and configure.ml	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \	Merge PR#740: Refactor documentation of records.	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Add tests for handling of warnings	Tej Chajed	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix bug 5392: Warnings defined in plugins are considered unknown	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \|_\|/ / / / / \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	In enter_one, not having exactly one goal is a fatal error of the monad.	Hugo Herbelin	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Pointed out by PMP.
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Add test-suite file for funind, extraction with compat 8.6	Jason Gross	2017-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Put plugin exports in the right compatibility file	Jason Gross	2017-06-22
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7.
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	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.
\| \| \| \| \| * \| \| \| \| \| \|	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.
\| * \| \| \| \| \| \| \| \| \|	[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")
\| \| \| \| \| \| \| \| * \|	Default colors for CoqIDE are actually applied.	Cyprien Mangin	2017-06-20
\| \| \| \| \| \|_\|_\|/ / \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes bug #5380 in particular. More generally, tags were not updated to the correct default value if the corresponding line in the configuration file was missing.
\| * \| \| \| \| \| \| \|	[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#812: Use more neutral wording instead of mentioning CoqIDE	Maxime Dénès	2017-06-20
\| \| \| \|\ \ \ \ \
* \| \| \| \ \ \ \ \	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#792: Fix ci-fiat-crypto to have a proper lite target	Maxime Dénès	2017-06-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Change CoqIDE-specific to neutral wording	Paul Steckler	2017-06-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \|