coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| * \| \| \| \| \| \| \|	[ide] Correctly place warning tags.	Emilio Jesus Gallego Arias	2017-04-08
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	8e07227c5853de78eaed4577eefe908fb84507c0 introduced an incorrect duplicate of `position_error_tag_at_sentence`, which sets the end of the underlining position starting at the end of the sentence, whereas the location in the feedback refers to the beginning, thus it highlights more text than it should. This was missed in 8.6 as it seems that the code was not called. We undo the duplication and fix the bug.
* \| \| \| \| \| \| \| \|	Update the .mailmap file.	Guillaume Melquiond	2017-04-08
\| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	Fix a heuristic used by legacy typeclass resolution.	Pierre-Marie Pédrot	2017-04-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The evarmap used by the heuristic could contain resolved evars, which could lead to a failure of backtracking in the EConstr branch. This is experimental and may be to costly.
\| \| \| \| \| \| \| * \|	[stm] remove process_error_hook	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`process_error_hook` seems unnecesary, we just call the proper error interpretation.
\| \| \| \| \| \| \| * \|	[stm] remove tactic_being_run hook	Emilio Jesus Gallego Arias	2017-04-07
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`tactic_being_run_hook` was used for the "xml" pluging but I am not sure we have a sensible use case here.
* \| \| \| \| \| \| \|	Merge PR#461: [camlpX] Remove camlp4 compat layer.	Maxime Dénès	2017-04-07
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	[toplevel] Remove the feedback feeder printing only on exit.	Emilio Jesus Gallego Arias	2017-04-07
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes the bug in `Drop` reported by @mattam82: after performing a `Drop`, the feeder was lost and no further message from Coq was printed.
\| \| \| * \| \| \| \|	Fix an unhandled exception in Omega.	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)	Matthieu Sozeau	2017-04-07
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR#485: Document Show Match	Maxime Dénès	2017-04-07
\|\ \ \ \ \ \ \ \
\| \| \| \| * \ \ \ \	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \|\ \ \ \ \ \| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Remove a forgotten rule for decl_mode from the Makefile.	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was making the miniopt target fail.
\| \| \| * \| \| \| \| \|	Turning the printing primitive projection parameter flag off by default.	Hugo Herbelin	2017-04-07
\| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	Turning the printing primitive projection compatibility flag off by default.	Hugo Herbelin	2017-04-07
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	[travis] Overlay for PR#461: Camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	[camlpX] Enrico's changes to camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This removes some remaining support for camlp4 in the infrastructure and documents the change.
\| \| * \| \| \| \| \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* \| \| \| \| \| \|	Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ↵	Maxime Dénès	2017-04-07
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	printer.
* \ \ \ \ \ \ \	Merge PR#519: Faster side effects	Maxime Dénès	2017-04-07
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Inline the only use of hcons_j in Term_typing.	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#488: Adding a documentation for the new proof engine.	Maxime Dénès	2017-04-06
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Adding a documentation for the new proof engine.	Pierre-Marie Pédrot	2017-04-06
\|/ / / / / / / / / /
\| \| * \| \| \| \| \| \| \|	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.
\| \| \| \| \| \| \| \| * \| \|	Factor interp_instance out of Pretyping.pretype_global	Gaetan Gilbert	2017-04-06
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	Avoid strange shadowing of Pretyping.interp_universe_level_name	Gaetan Gilbert	2017-04-06
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	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.