coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| * \| \| \| \|	Documenting the fact terms are only hashconsed outside of a section.	Pierre-Marie Pédrot	2017-04-06
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	Fix a normalization hotspot in computation of constr keys.	Pierre-Marie Pédrot	2017-04-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT.
* \| \| \| \| \| \| \|	Merge PR#542: [travis] Add webhook to Gitter.	Maxime Dénès	2017-04-06
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	[travis] Add webhook to Gitter.	Théo Zimmermann	2017-04-06
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	[toplevel] Remove exception error printer in favor of feedback printer.	Emilio Jesus Gallego Arias	2017-04-05
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
\| \| \| \| \| \| * \|	Removing a normalization hotspot from EConstr.	Pierre-Marie Pédrot	2017-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was not necessary to normalize a term just to check whether it was a global reference. The hotspot appeared in mathcomp.
* \| \| \| \| \| \| \|	Merge PR#434: Optimizing array mapping in the kernel.	Maxime Dénès	2017-04-05
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| *	Adding tests for chained abstract tactics.	Pierre-Marie Pédrot	2017-04-04
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| *	Fix substitution of abstracted lemmas.	Pierre-Marie Pédrot	2017-04-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of browsing the term as many times as there are abstracted constants, we replace the constants in one pass. We have to be a bit careful to replace the right variables though, in case there are chained abstracts. This is much faster. This solves the second part of bug #5382: Huge case analysis fails in coq8.5.x.
* \| \| \| \| \| \| \| \|	Merge PR#502: [pp] Add anomaly header to error messages.	Maxime Dénès	2017-04-04
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\| \| \| \| \| \| \| \| \|\ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-03
\|\ \ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \	Merge PR#533: Instances should obey universe binders even when defined by ↵	Maxime Dénès	2017-04-03
\| \|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tactics.
* \| \| \| \| \| \| \| \| \| \|	Fix loading of ocamldebug printers.	Pierre-Marie Pédrot	2017-04-03
\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \|	Instances should obey universe binders even when defined by tactics.	Gaetan Gilbert	2017-04-03
\| \|/ / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR#417: No cast surgery in let in	Maxime Dénès	2017-04-03
\|\ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \|	Add test file for #4957.	Maxime Dénès	2017-04-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly".
* \| \| \| \| \| \| \| \| \| \|	Fix higher-order pattern variables not being printed as "@?" (bug #5431).	Guillaume Melquiond	2017-04-02
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Fix documentation typo (bug #5433).	Guillaume Melquiond	2017-04-02
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Simplify some proofs.	Guillaume Melquiond	2017-04-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing.
\| \| \| \| \| \| \| \| \| \| *	Restore a fast path in EConstr instance normalization.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* \| \| \| \| \| \| \| \| \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For now we only normalize sorts, and we leave instances for the next commit.
\| \| \| \| \| \| \| \| \| \| *	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	Ensuring proper cast invariants in EConstr.kind.	Pierre-Marie Pédrot	2017-03-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The kernel does fishy things with casts, such that ensuring there are no two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr view as well.
\| \| \| \| \| \| \| \| \| \| *	Revert "Specially crafted EConstr.kind to be more efficient."	Pierre-Marie Pédrot	2017-03-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance difference was not conclusive enough to pay for the code ugliness.
\| \| \| \| \| \| \| \| \| \| *	Specially crafted EConstr.kind to be more efficient.	Pierre-Marie Pédrot	2017-03-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We do one step of loop unrolling, limit the number of allocations and mark the function as inline.
* \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-30
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \|/ / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Merge PR#463: Run non-tactic comands without resilient_command	Maxime Dénès	2017-03-30
\| \|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \|	Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.	Guillaume Melquiond	2017-03-30
\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR#469: Added take to VectorDef	Maxime Dénès	2017-03-30
\|\ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \|	Added take to VectorDef.	George Stelle	2017-03-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties.
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#511: [stm] Remove some obsolete vernacs/classification.	Maxime Dénès	2017-03-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#522: [coqide] Protect against size_allocate race in proofview.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|/ / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR#514: [travis] Backport from trunk: VST	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \| \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#521: Do so that "About" tells if a reference is a coercion.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#525: [ide] Fix typo in pp serialization.	Maxime Dénès	2017-03-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|\ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix call to broken unsafe_type_of in apply tactic.	Maxime Dénès	2017-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This broke the build of iris-coq in the EConstr branch. Each time you use unsafe_type_of, I loose a night of sleep, so please stop.
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Run non-tactic comands without resilient_command	Tej Chajed	2017-03-29
\| \| \| \| \| \|_\|_\|_\|/ / / / / / / / / \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ide] Fix typo in pp serialization.	Emilio Jesus Gallego Arias	2017-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Revert to incorrect heuristic in apply.	Maxime Dénès	2017-03-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was breaking e.g. fiat-crypto.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixing missing PropFacts.v in Logic/vo.itarget.	Hugo Herbelin	2017-03-28
\|/ / / / / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is while waiting for a possible different solution, if ever such a different solution is adopted, since the coq.inria.fr/library has currently a broken link and someone rightly complained about it.
\| \| \| \| \| * / / / / / / / / / /	[coqide] Protect against size_allocate race in proofview.	Emilio Jesus Gallego Arias	2017-03-28
\| \|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	To handle dynamic printing in CoqIDE we listen to the `size_allocate` signal , [see more details in 6885a398229918865378ea24f07d93d2bcdd2802] However, we must be careful to protect against scrollbar creation: it is possible for the `size_allocate` handler to change the size when inserting text (due to scrollbars), thus we may enter in an infinite loop. Our fix is to check if the width has really changed, as done in `Wg_MessageView`. This fixes the problem noted by @herbelin in https://coq.inria.fr/bugs/show_bug.cgi?id=5417
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Do so that "About" tells if a reference is a coercion.	Hugo Herbelin	2017-03-27
\|/ / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| * \| \|	More efficient check in validity of side-effects.	Pierre-Marie Pédrot	2017-03-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We don't need to look for the size of the whole list to find whether we can extract a suffix from it, as we can do it in one go instead. This slowness was observable in abstract-heavy code.