coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Minor cosmetic commit.	Hugo Herbelin	2017-04-09
\|
*	Documenting how the recursive indices of a fixpoint are computed.	Hugo Herbelin	2017-04-09
\| \| \| \|	Also documenting how the implicit arguments by position are computed.
*	More explicit message when a {struct x} argument refers to a local definition.	Hugo Herbelin	2017-04-09
\|
*	Removing internal support for accepting "{struct x}" and co in "Theorem with".	Hugo Herbelin	2017-04-09
\| \| \| \| \|	There were actually no syntax for it, and I'm still unsure what good syntax to give to it, even more that it would be useful to have one.
*	Update the .mailmap file.	Guillaume Melquiond	2017-04-08
\|
*	Merge PR#461: [camlpX] Remove camlp4 compat layer.	Maxime Dénès	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
\|\ \
* \| \|	Remove a forgotten rule for decl_mode from the Makefile.	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \|	This was making the miniopt target fail.
\| \| *	[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
\|\ \ \ \ \
* \ \ \ \ \	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
* \| \| \| \| \|	Merge PR#434: Optimizing array mapping in the kernel.	Maxime Dénès	2017-04-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#502: [pp] Add anomaly header to error messages.	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.
* \| \| \| \| \| \| \| \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.