coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| * \| \|	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.
\| * \| \| \| \| \| \|	[toplevel] Fix #5475	Emilio Jesus Gallego Arias	2017-04-18
\|/ / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e, `Notice`-level messages should not be wrapped in `<infomsg>` tags.
\| * / / / / /	Adding and fixing links in README.	Théo Zimmermann	2017-04-18
\|/ / / / / /
* \| \| \| \| \|	Add a test for bug #5321: clearbody breaks typing of goal.	Pierre-Marie Pédrot	2017-04-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The bug has been solved as a side-effect of the EConstr branch.
* \| \| \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\ \ \ \ \ \ \| \| \|/ / / / \| \|/\| \| \| \|
* \| \| \| \| \|	Merge PR#523: [readme] Add badges for Travis and Gitter.	Maxime Dénès	2017-04-15
\|\ \ \ \ \ \
\| \| * \| \| \| \|	Fixing bug #5470 (anomaly on notations with misused "binder" type).	Hugo Herbelin	2017-04-14
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Fixing bug #5469 (notation format not recognizing curly braces).	Hugo Herbelin	2017-04-14
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Fix EOL characters in xml protocol documentation.	Maxime Dénès	2017-04-14
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.	Maxime Dénès	2017-04-14
\| \| \|\ \ \ \ \
\| \| \| * \| \| \| \|	Fix anomaly when doing [all:Check _.] during a proof.	Gaetan Gilbert	2017-04-14
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR#557: [toplevel] Don't print goals if there is no pending proof.	Maxime Dénès	2017-04-14
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#554: Update INSTALL now that -debug is the default.	Maxime Dénès	2017-04-14
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \ \ \ \ \	Merge PR#563: add XML protocol doc for 8.6	Maxime Dénès	2017-04-14
\| \| \| \| \|\ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \|	[travis] Use the lite target for fiat-crypto.	Maxime Dénès	2017-04-14
\| \| \| \| \| \|/ / / / / \| \| \| \| \|/\| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR#559: Fix compilation with camlp5 transitional mode.	Maxime Dénès	2017-04-14
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Fix compilation with camlp5 transitional mode.	Maxime Dénès	2017-04-14
\|/ / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was failing after 1d0eb5d4d6fea.
\| \| \| \| \| * \| \| \| \|	update XML protocol doc to 8.6	Paul Steckler	2017-04-13
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	add XML protocol doc for 8.5	Paul Steckler	2017-04-13
\| \| \| \| \|/ / / / /
\| \| * \| \| \| \| \| \|	[toplevel] Don't print goals if there is no pending proof.	Emilio Jesus Gallego Arias	2017-04-13
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Silence a few OCaml warnings.	Guillaume Melquiond	2017-04-13
\| \|/ / / / / / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Merge PR#510: Correctly identify [Time Defined.] as a defined	Maxime Dénès	2017-04-12
\| \| \| \|\ \ \ \ \
* \| \| \| \ \ \ \ \	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	[toplevel] [stm] cleanup in module open	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	[stm] [nit] Centralize compile-time debug flag.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	[stm] Improve error messages on add/parse.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As suggested by @psteckler in #524 , we give more explicit information about what is wrong. We also provide some debug information for the possible dangerous case of having the tip go out of sync with the real installed state (which will make parsing fail if there was some changes to the parser). We also fix a couple of typos noticed by Paul, thanks Paul.
\| * \| \| \| \| \| \| \| \|	[flags] Documentation and a minor tweak.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Mostly documentation and making a couple of local flags, local.
\| * \| \| \| \| \| \| \| \|	[vernac] vernacentries.mli cleanup	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This header file had accumulated quite a bit of cruft over the years, we clean it up while we are at it. No functional change as all the removed variables/methods were noops long time ago.
\| * \| \| \| \| \| \| \| \|	[stm] Port the toplevel to the STM.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled.
\| * \| \| \| \| \| \| \| \|	[stm] Move main parsing entry point to the STM.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Mainly due to notations, proof modes and plugins, parsing in Coq is stateful, so we expose a state-aware parsing API in the STM. This is a first move to unify all the parsing entry points in the Stm and the toplevel, and allows STM clients to control their input stream properly. This greatly helps for instance, with whole-document parsing. This commit supersedes PR#204.
\| * \| \| \| \| \| \| \| \|	[stm] Remove edit_id.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203.
* \| \| \| \| \| \| \| \| \|	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵	Maxime Dénès	2017-04-12
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	record fields.
* \ \ \ \ \ \ \ \ \ \	Merge PR#549: Fast path in weak head reduction of applied atoms.	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \|	Update INSTALL now that -debug is the default.	Théo Zimmermann	2017-04-11
\| \|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also updates the references to debugging documentation.
* \| \| \| \| \| \| \| \| \| \|	Merge PR#543: Sanitize instance interpretation	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#532: Clean Nsatz implementation.	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#537: Efficient side-effect abstraction	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding a test for 'rewrite in *' when an evar is solved by side-effect.	Pierre-Marie Pédrot	2017-04-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding a test for the correctness of normalization in legacy typeclasses.	Pierre-Marie Pédrot	2017-04-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Documenting the changes introduced by the EConstr branch.	Pierre-Marie Pédrot	2017-04-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Revert "refactoring: Reductionops.contextual_reduction_function type"	Matej Košík	2017-04-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Revert "comment: typo"	Matej Košík	2017-04-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6.