coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵	Maxime Dénès	2017-11-13
\|\ \| \| \| \| \| \|	type is unknown
* \	Merge PR #6117: Fix printing anomaly in conv	Maxime Dénès	2017-11-13
\|\ \
* \ \	Merge PR #6103: Hack to restore printing of glob_constr in debugger.	Maxime Dénès	2017-11-13
\|\ \ \
* \ \ \	Merge PR #6088: Remove packaging scripts while waiting for a fix to #5998.	Maxime Dénès	2017-11-13
\|\ \ \ \
* \ \ \ \	Merge PR #6071: [ci] Add Ltac2	Maxime Dénès	2017-11-13
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| *	Adding a debugging printer for ident maps whose codomain type is unknown.	Hugo Herbelin	2017-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer.
* \| \| \| \| \| \| \| \|	Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6096: Documentation: "tac1 \|\| tac2" means "first [ progress tac1 \| ↵	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tac2 ]"
* \ \ \ \ \ \ \ \ \ \	Merge PR #6087: [feedback] Helper to print feedback messages in the console.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6086: [ci] Switch VST back to upstream.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| *	Fixing missing separator in an error message.	Hugo Herbelin	2017-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The message is the "Conversion test raised an anomaly" one.
\| \| \| \| \| \| \| \| \| \| \| \| *	Fixing an (apparently misplaced) spc in anomaly reporting message.	Hugo Herbelin	2017-11-08
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| *	Hack to restore printing of glob_constr in debugger.	Hugo Herbelin	2017-11-07
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \|	[api] Remove 8.7 ML-deprecated functions.	Emilio Jesus Gallego Arias	2017-11-07
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \|	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will allow to merge back `Names` with `API.Names`
* \| \| \| \| \| \| \| \|	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \|	Documentation: "tac1 \|\| tac2" means "first [ progress tac1 \| tac2 ]",	Samuel Gruetter	2017-11-06
\| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	not "first [ progress tac1 \| progress tac2 ]". And add a missing backslash.
\| \| \| \| \| \| \| \| *	Remove packaging scripts while waiting for a fix to #5998.	Théo Zimmermann	2017-11-06
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a temporary commit which should be reverted once the issue is fixed.
\| \| \| \| * \| \| \|	[feedback] Helper to print feedback messages in the console.	Emilio Jesus Gallego Arias	2017-11-06
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is useful for tools such as `coqchk` or `coq_makefile` that want to handle feedback on their own.
* \| \| \| \| \| \|	Merge PR #6072: Protecting evar map printer	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	alphabet).
* \ \ \ \ \ \ \ \	Merge PR #6085: Update .mailmap with a jkloos alias	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6063: Finish removing Show Goal uid	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	rules
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #1139: Add a linter.	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \|	Update .mailmap with a jkloos alias	Jason Gross	2017-11-05
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \|	Refining PR#924 (insensitivity of projection heuristics to alphabet).	Hugo Herbelin	2017-11-05
\| \|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
\| \| \| \| * \| \| \| \| \| \|	Cosmetic changes in evar_map printer.	Hugo Herbelin	2017-11-05
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Preventively protect locally against failures of evar_map printer.	Hugo Herbelin	2017-11-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It is not clear that this is really needed, but in case it happens, one will at least have a partial result available rather than an unexploitable global failure of the parser.
\| \| \| \| * \| \| \| \| \| \|	Fixing a cause of failure of evar_map printer in debugger.	Hugo Herbelin	2017-11-05
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Indeed, the debugger debugs coqtop but it is itself just an ocaml runtime extended with the coq printers. It does not know the environment, so, looking in the Global.env() for the printers can only fail.
\| \| \| \| \| \| \| \| \| *	[ci] Add Ltac2	Jason Gross	2017-11-04
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a first step towards some of the solutions proposed in #6008.
\| \| \| * \| \| \| \|	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
\| \|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
\| \| \| \| \| * \|	Adding support for syntax "let _ := e in e'" in Ltac.	Hugo Herbelin	2017-11-04
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding a file fixing #5996 and which uses this feature.
* \| \| \| \| \|	Merge PR #6060: Improve error message and fix #6055 (spelling mistake).	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	variables).
* \ \ \ \ \ \ \ \ \	Merge PR #6036: [toplevel] Export the last document seen after `Drop`.	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	dev/doc/changes.
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6024: Update of Coq version history	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ↵	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	color in coqide).
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	alphabet
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Update tactics.ml	Farzon Lotfi	2017-11-02
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person.