coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| * \| \| \| \| \| \| \| \| \|	kernel: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \|	Use whd-all on rigid-flex conversion.	Pierre-Marie Pédrot	2018-02-02
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6670: Delete duplicate line	Maxime Dénès	2018-02-01
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...	Maxime Dénès	2018-02-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6672: [stm] Move options to a per-document record.	Maxime Dénès	2018-02-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6660: [lib] Respect change of options under with/without_option.	Maxime Dénès	2018-02-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[vernac] Mutual theorems (VernacStartTheoremProof) always have names	Vincent Laporte	2018-02-01
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition	Vincent Laporte	2018-02-01
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	CI: Run coqchk on Iris	Ralf Jung	2018-01-31
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Proofview: enter_one: add __LOC__ argument to get relevant error msg	Enrico Tassi	2018-01-31
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	[stm] Move options to a per-document record.	Emilio Jesus Gallego Arias	2018-01-31
\| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6601: Circle CI: fix cache selection.	Maxime Dénès	2018-01-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m...	Maxime Dénès	2018-01-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6663: [toplevel] Refactor load path handling.	Maxime Dénès	2018-01-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"	Maxime Dénès	2018-01-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.	Maxime Dénès	2018-01-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Delete duplicate line	Paul Steckler	2018-01-30
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[lib] Respect change of options under with/without_option.	Emilio Jesus Gallego Arias	2018-01-30
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Put default value for NJOBS in ci-common.	Gaëtan Gilbert	2018-01-30
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding an overlay for Equations.	Pierre-Marie Pédrot	2018-01-30
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6666: Fix reduction of primitive projections on coinductive records...	Maxime Dénès	2018-01-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections	Maxime Dénès	2018-01-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6636: Stop running duplicate Travis jobs on pull requests.	Maxime Dénès	2018-01-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6605: Safer VM interfaces	Maxime Dénès	2018-01-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6644: Use travis_retry on apt-get update	Maxime Dénès	2018-01-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add test case for #5286.	Maxime Dénès	2018-01-29
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[cbv] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[native_compute] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[toplevel] Refactor load path handling.	Emilio Jesus Gallego Arias	2018-01-29
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	allow vernacular controls before focus selector, issue #6587	Paul Steckler	2018-01-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Support universe instances on the literal Type	Tej Chajed	2018-01-26
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	document the Fail command	Paul Steckler	2018-01-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Add test case for #5747	Maxime Dénès	2018-01-25