coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	detype_case predicate is not optional	Gaëtan Gilbert	2018-02-14
\|
*	Merge PR #6738: CHANGES for universe variance	Maxime Dénès	2018-02-13
\|\
* \	Merge PR #6565: [Backport script] Check .mli files are not changed.	Maxime Dénès	2018-02-12
\|\ \
* \ \	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\ \ \
\| \| \| *	CHANGES for universe variance	Gaëtan Gilbert	2018-02-12
\| \| \| \|
* \| \| \|	Merge PR #6262: [error] Replace msg_error by a proper exception.	Maxime Dénès	2018-02-12
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #1047: Support universe instances on the literal Type	Maxime Dénès	2018-02-12
\|\ \ \ \
* \ \ \ \	Merge PR #6128: Simplification: cumulativity information is variance ↵	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	information.
* \ \ \ \ \	Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6418: More detailed error messages for Canonical Structure, #6398	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6139: Make list functions returning sumbools transparent	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6718: Fix redirection to stderr in lint-repository error message.	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6708: Mention -quiet flag for Fail	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6706: ci-common: guess CI_BRANCH for local builds	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6674: Delay computation of lifts in the reduction machine.	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \|	inferCumulativity: add comment to explain [if not is_arity].	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Documentation for cumulative inductive variance.	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Print inductive cumulativity info in About.	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Universe instance printer: add optional variance argument.	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This ensures by construction that we never infer constraints outside the variance model.
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert	2018-02-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j k \|= )
\| \| \| \| \| \| \| \| \| * \| \| \| \|	[get_cumulativity_constraints] allowing further code sharing.	Gaëtan Gilbert	2018-02-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Factorize code for comparing maybe-cumulative inductives.	Gaëtan Gilbert	2018-02-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it.
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix typo in Univ.CumulativityInfo	Gaëtan Gilbert	2018-02-10
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \|	[error] Replace msg_error by a proper exception.	Emilio Jesus Gallego Arias	2018-02-09
\| \| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
\| \| \| \| \| \| \| \| * \| \| \|	[nativecomp] Remove ad-hoc handling of Dynlink exception.	Emilio Jesus Gallego Arias	2018-02-09
\| \|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead, we properly register a printer for such exception and update the code.
\| \| \| \| \| * \| \| \| \| \|	Fix redirection to stderr in lint-repository error message.	Gaëtan Gilbert	2018-02-08
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	mention interactive mode for Fail message	Paul Steckler	2018-02-07
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6657: Document the Fail command	Maxime Dénès	2018-02-07
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6685: Use whd-all on rigid-flex conversion.	Maxime Dénès	2018-02-07
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6610: Points to Flocq official repository.	Maxime Dénès	2018-02-07
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6673: Fix evar handling in native_compute conversion	Maxime Dénès	2018-02-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \|	ci-common: guess CI_BRANCH for local builds	Gaëtan Gilbert	2018-02-07
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	More detailed error messages for Canonical Structure, #6398	Paul Steckler	2018-02-06
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.	Maxime Dénès	2018-02-06
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6695: [toplevel] Refine start of interactive mode conditions.	Maxime Dénès	2018-02-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \|	Points to Flocq official repository.	Théo Zimmermann	2018-02-05
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
\| \| \| \| \| * \| \| \| \| \| \| \|	Respect the transparent state of the current conversion on strong weak-head.	Pierre-Marie Pédrot	2018-02-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state.
\| \| \| \| * \| \| \| \| \| \| \| \|	Add overlay for equations (nf_beta takes an env)	Gaëtan Gilbert	2018-02-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	[native_compute] Remove useless conversion to list in reification.	Maxime Dénès	2018-02-05
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in ↵	Maxime Dénès	2018-02-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	VernacDefinition
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6654: CI: Run coqchk on Iris	Maxime Dénès	2018-02-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6652: Allow vernacular controls before focus selector	Maxime Dénès	2018-02-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[stm] [toplevel] Make loadpath a parameter of the document.	Emilio Jesus Gallego Arias	2018-02-05
\| \| \| \| \|/ / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc...
\| \| \| \| * / / / / / / / / /	[toplevel] Refine start of interactive mode conditions.	Emilio Jesus Gallego Arias	2018-02-05
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Refinement of the toplevel codepath requires to be more careful about the conditions for coqtop to be interactive. Fixes #6691. We also tweak the vio auxiliary function.
\| \| \| \| \| \| \| * \| \| \| \| \|	Delay computation of lifts in the reduction machine.	Pierre-Marie Pédrot	2018-02-04
\| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This definitely qualifies as a micro-optimization, but it would not be performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml semantics, as it involves a fixpoint and changes potential non-termination. In our case it doesn't matter semantically, but it is indeed observable on computation intensive developments like UniMath.