| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
|
Was lost during the coq_makefile 1 -> 2 translation.
|
|
|
|
|
|
And some code simplification.
|
|
And a bit of code simplification.
|
|
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
|
This brings us one step closer to actually moving all STM flags to
`stm`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.
This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.
Fixes #6364.
|
|
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
|
compatible change.
|
|
|
|
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
|
|
|
|
|
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|
Together with #1122, this makes `VernacInstance` the only command in
the Coq codebase that cannot be statically determined to open a proof.
The reasoning for the commands moved to `VtSideff` is that
parser-altering commands should be always marked `VtNow`; the rest can
be usually marked as `VtLater`.
|
|
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
|
|
In the transition towards a less global state handling we have the
necessity of mix imperative setting [notably for the modules/section
code] and functional handling of state [notably in the STM].
In that scenario, it is very convenient to have typed access to the
Coq's `summary`. Thus, I reify the API to support typed access to the
`summary`, and implement such access in a couple of convenient places.
We also update some internal datatypes to simplify the `frozen` data
type. We also remove the use of hashes as it doesn't really make
things faster, and most operations are now over `Maps` anyways.
I believe this goes in line with recent work by @ppedrot.
We also deprecate the non-typed accessors, which were only supposed to
be used in the STM, which is now ported to the finer primitives.
|
|
|
|
They were not used anymore since the previous patches.
|
|
|
|
Currently, `make ci-sf` downloads and builds the files in the main root
directory. we fix that.
|
|
Committed on master by mistake. Clearly I'm too clumsy to be trusted
with push rights.
This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
|
|
|
|
As noted in the bug #6291, `.cmx` files are not installed in the
coqlib, which yields the warning:
```
Warning 58: no cmx file was found in path for module Sorts, and its
interface was not compiled with -opaque
```
We thus install the `cmx` files to fix this problem, and also install
the `.o` files for plugins' `.o` to support linking the plugins
statically.
This closes #5099 and #6291.
|
|
|
|
|
|
|
|
|
|
source.
|
|
Closes #6194 .
|
|
|
|
|
|
Funnily enough, the old code is completely bogus. It succeeds in early files
of the prelude just because the heterogeneous equality has not been required.
This raises an exception which is not the same one as if we tried to rewrite
with the identity type first.
The only user, the inversion tactic, was actually only relying on Logic.eq
and was furthermore not even using the convertibility algorithm. We just
perform a syntactic match now.
|
|
|
