coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	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 informa...	Maxime Dénès	2018-02-12
\|\ \ \
* \ \ \	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
\| \| \| \| \| \| \| \| \| * \| \|	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
\| \| \| \| \| \| \| \| \| * \| \|	[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
\| \| \| \| \| \| \| \| \| * \| \|	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
\| \| \| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \| \| \|/\|
\| \| \| \| \| \| \| \| * \|	[nativecomp] Remove ad-hoc handling of Dynlink exception.	Emilio Jesus Gallego Arias	2018-02-09
\| \|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	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
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \|	Respect the transparent state of the current conversion on strong weak-head.	Pierre-Marie Pédrot	2018-02-05
\| \| \| \| * \| \| \| \| \| \|	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 Ve...	Maxime Dénès	2018-02-05
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	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
\| \| \| \| \|/ / / / / / / /
\| \| \| \| * / / / / / / /	[toplevel] Refine start of interactive mode conditions.	Emilio Jesus Gallego Arias	2018-02-05
\| \|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \|	Delay computation of lifts in the reduction machine.	Pierre-Marie Pédrot	2018-02-04
\| \|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	CClosure.unfold_projection: don't catch Not_found, assume env is ok	Gaëtan Gilbert	2018-02-02
\| \| \| \| * \| \| \| \| \|	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
\| \| \| \| * \| \| \| \| \|	checker: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\| \| \| \| * \| \| \| \| \|	checker: remove unused per-constant reduction flags.	Gaëtan Gilbert	2018-02-02