coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| \| * \| \| \| \| \| \| \| \| \|	CClosure.unfold_projection: don't catch Not_found, assume env is ok	Gaëtan Gilbert	2018-02-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We can do this after the parent commit (Reductionops.nf_* don't use empty env)
\| \| \| \| * \| \| \| \| \| \| \| \| \|	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \|	checker: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This just shares the unfold_projection between Closure and Reduction.
\| \| \| \| * \| \| \| \| \| \| \| \| \|	checker: remove unused per-constant reduction flags.	Gaëtan Gilbert	2018-02-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \|	kernel: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- use Redflags.red_projection - share unfold_projection between CClosure and Reduction
\| \| \| \| * \| \| \| \| \| \| \| \|	Use whd-all on rigid-flex conversion.	Pierre-Marie Pédrot	2018-02-02
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This heuristic is justified by the fact that during a conversion check between a flexible and a rigid term, the flexible one is eventually going to be fully weak-head normalized. So in this case instead of performing many small reduction steps on the flexible term, we perform full weak-head reduction, including delta. It is slightly more efficient in actual developments, and it fixes a corner case encountered by Jason Gross. Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
* \| \| \| \| \| \| \| \| \| \| \|	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 ↵	Maxime Dénès	2018-02-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	error msg
* \ \ \ \ \ \ \ \ \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The type discipline of the tactic monad does not distinguish between mono-goal and multi-goal tactics. Unfortunately enter_one "asserts false" if called on 0 or > 1 goals. The __LOC__:string argument can be used to make the error message more helpful (since the backtrace is pointless inside the monad). The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..". The __LOC__ variable is filled in by the OCaml compiler with the current file name and line number.
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	[stm] Move options to a per-document record.	Emilio Jesus Gallego Arias	2018-01-31
\| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We gather (almost) all the STM options in a record, now set at document creation time. This is refactoring is convenient for some other ongoing functionalization work.
* \| \| \| \| \| \| \| \| \| \| \| \| \|	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 ↵	Maxime Dénès	2018-01-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	menhir.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	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
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The old semantics of `with/without_option` allowed the called function to modify the value of the option. This is an issue mainly with the `silently/verbose` combinators, as `Set Silent` can be executed under one of them and thus the modification will be lost in the updated code introduced in a554519874c15d0a790082e5f15f3dc2419c6c38 IMHO these kind of semantics are quite messy but we have to preserve them in order for the `Silent` system to work. In fact, note that in the previous code, `with_options` was not consistent with `with_option` [maybe that got me confused?] Ideally we could restore the saner semantics once we clean up the `Silent` system [that is, we remove the flag altogether], but that'll have to wait. Fixes #6645.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	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 ↵	Maxime Dénès	2018-01-30
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	records for cbv and native_compute
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #5286 (last remaining part).
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[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
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We refactor top-level load path handling. This is in preparation to make load paths become local to a particular document. To this effect, we introduce a new data type `coq_path` that includes the full specification of a load path: ``` type add_ml = AddNoML \| AddTopML \| AddRecML type vo_path_spec = { unix_path : string; (* Filesystem path contaning vo/ml files ) coq_path : Names.DirPath.t; ( Coq prefix for the path ) implicit : bool; ( [implicit = true] avoids having to qualify with [coq_path] ) has_ml : add_ml; ( If [has_ml] is true, the directory will also be search for plugins *) } type coq_path_spec = \| VoPath of vo_path_spec \| MlPath of string type coq_path = { path_spec: coq_path_spec; recursive: bool; } ``` Then, initialization of load paths is split into building a list of load paths and actually making them effective. A future commit will make thus the list of load paths a parameter for document creation. This API is necessarily internal [for now] thus I don't think a changes entry is needed.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes BZ#5726.
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.