coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fast path when checking equality of universe levels in UState.	Pierre-Marie Pédrot	2017-04-27
\| \| \| \| \|	We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes.
*	Code cleaning in unification algorithm for universes.	Pierre-Marie Pédrot	2017-04-27
\| \| \| \| \| \| \|	This patch is only moving code around and expliciting statically the invariants of the functions, so it should be 1:1 equivalent to the other one. Amongst other goodies, the unification function is not recursive anymore, which ensures that it will terminate.
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-04-27
\|\
\| *	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
\| \| \| \| \| \| \| \| \| \| \| \|	Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails.
* \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
\| \| \| \| \| \| \| \| \| \| \| \|	Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails.
\| *	Merge PR#567: Fix bug #5377: @? patterns broken.	Maxime Dénès	2017-04-25
\| \|\
* \| \	Merge PR#578: Fix nsatz not recognizing real literals.	Maxime Dénès	2017-04-25
\|\ \ \
* \ \ \	Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.	Maxime Dénès	2017-04-24
\|\ \ \ \
* \ \ \ \	Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.	Maxime Dénès	2017-04-24
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#552: Miscelaneous commits	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \
\| \| \| \| \| * \	Merge PR#577: Add bedrock targets src and facade to Travis CI	Maxime Dénès	2017-04-24
\| \| \| \| \| \|\ \
* \| \| \| \| \| \ \	Merge PR#569: Documenting EConstr for developpers.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#565: Remove VernacError	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#576: [ide] Rely less on `Stateid.dummy`	Maxime Dénès	2017-04-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \|	[travis] Pin camlp5 to the minimal version 6.14 for 4.02.3	Emilio Jesus Gallego Arias	2017-04-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We now test: - 4.02.3 + 6.14 [and 32bits of those] - 4.04.0 + 6.17 this looks like what the official support set should be for 8.7, given that both Ubuntu and Debian will ship the first, then switch to the latter. We also pin xmlm to version 1.2.0 to workaround bug https://github.com/ocaml/opam-repository/issues/8815
\| \| \| * \| \| \| \| \| \| \| \| \| \|	[toplevel] [emacs] Don't quote errors in emacs mode.	Emilio Jesus Gallego Arias	2017-04-23
\| \| \|/ / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. We also update the warnings quoter to use a warning tag instead of a non-printable char. This fixes ProofGeneral for trunk users. c.f. https://github.com/ProofGeneral/PG/issues/175
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge branch v8.6 into trunk	Hugo Herbelin	2017-04-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
* \| \| \| \| \| \| \| \| \| \| \| \|	Removing TODO file which is unused for more than 10 years.	Hugo Herbelin	2017-04-22
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Hoping this is ok for everyone, otherwise we can discuss about it.
\| \| \| * \| \| \| \| \| \| \| \|	[ide] Fix #5482 "location for query commands" in IDE.	Emilio Jesus Gallego Arias	2017-04-21
\| \|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This warning is a special case as it happens outside the execution context. We could move the check inside, but instead we opt for the simpler solution of properly setting the warning target.
\| \| \| * \| \| \| \| \| \| \|	Remove VernacError	Gaetan Gilbert	2017-04-21
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	[flags] Deprecate is_silent/is_verbose in favor of single flag.	Emilio Jesus Gallego Arias	2017-04-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
\| \| \| \| \| \| \| \| * \|	Add bedrock targets src and facade	Jason Gross	2017-04-20
\| \| \|_\|_\|_\|_\|_\|/ / \| \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \|	Fix nsatz not recognizing real literals.	Guillaume Melquiond	2017-04-20
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Fix bug #5377: @? patterns broken.	Pierre-Marie Pédrot	2017-04-20
\| \| \|_\|_\|_\|_\|/ \| \|/\| \| \| \| \|
\| \| \| \| * \| \|	COMMENT: Pre_env.env	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	COMMENT: Proof_global.pstate.pid	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	refactoring "Ppvernac.pr_extend"	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	correcting a typo in a comment	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	correcting comments in the "Context" module	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	"tclENV" is sexier, use it instead of "Env.get"	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	reduce syntactic noise	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	simplifying "Environ.push_named" function	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	refactoring "Names.DirPath.is_empty" function	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	refactoring "Names.DirPath.compare" function	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	refactoring "Names.DirPath.equal" function	Matej Kosik	2017-04-20
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	correcting a typo in a comment	Matej Kosik	2017-04-20
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| * \| \| \|	[ide] Set Stateid in query pane.	Emilio Jesus Gallego Arias	2017-04-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We again remove another user of Stateid.dummy. However, we need to adapt the protocol so `Coq.query` takes the `route_id` and we can redirect the output properly to the subwindow.
\| \| * \| \| \|	[ide] Rely less on `Stateid.dummy`	Emilio Jesus Gallego Arias	2017-04-19
\| \| \| \|_\|/ \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, we set queries from the menu to the tip of the document, and process feedback coming with a `dummy` id. There are still more places to tweak, but this should be good for now. We also display a few more query messages, in particular the feedbacks produced by query that carry a dummy state id. This hack of reporting with from the STM should be solved once we update the protocol.
\| \| \| * \|	Documenting EConstr for developpers.	Pierre-Marie Pédrot	2017-04-19
\| \| \|/ /
\| \| \| *	Fix bug #5476: Ltac has an inconsistent view of hypotheses.	Pierre-Marie Pédrot	2017-04-19
\| \|_\|/ \|/\| \|
* \| \|	Merge PR#573: [toplevel] Fix printing of parsing errors + corner case.	Maxime Dénès	2017-04-19
\|\ \ \
* \| \| \|	CHANGES entry for #545.	Maxime Dénès	2017-04-19
\| \| \| \|
* \| \| \|	Merge PR#545: Add some hints to the "real" database to automatically ↵	Maxime Dénès	2017-04-19
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	discharge literal comparisons.
\| \| \| * \	Merge PR#538: Correction of bug #4306	Maxime Dénès	2017-04-19
\| \| \| \|\ \
* \| \| \| \ \	Merge PR#570: Adding and fixing links in README.	Maxime Dénès	2017-04-19
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#571: [toplevel] Fix #5475	Maxime Dénès	2017-04-19
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
\| \| \| \| * \| \|	[toplevel] Fix printing of parsing errors + corner case.	Emilio Jesus Gallego Arias	2017-04-19
\| \|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PR #441 and #530 had an interesting interaction creating two bugs: - #441 stopped emitting feedback for the parser, however #530 changed the mechanism to print parser errors to the feedback, thus when the two patches were applied, parsing errors were not printed in batch_mode. - Additionally, #530 contains an error: prior to `Stm.init` we must take care of exceptions `require ()`/etc... otherwise they won't get printed.