| Age | Commit message (Collapse) | Author |
|---|
|
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].
|
|
Instead, we properly register a printer for such exception and update
the code.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
|
|
This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
|
|
|
|
|
|
|
|
|
|
I don't understand what is wrong with putting a query in a script
running in the IDE. It is typically needed when giving demos, and that
sounds like a ligitimate use case. By the way, we do it ourselves every year
during the demo at CoqPL...
|
|
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
|
|
|
|
|
Typeclasses.typeclass
|
|
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
|
One less global flag.
|
|
|
|
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
|
We remove a few old-style normalization and try to use the newer APIs,
however, it is hard to say whether the right magic is being used.
|
|
|
|
|
|
This is useful as it allows to reflect program_mode behavior as an attribute.
|
|
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
|
|
|
|
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
|
|
|
|
|
|
|
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
|
|
|
|
|
|
|
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.
|
|
|
|
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
|
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.
|
|
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
|
|
|
|
In particular we must invalidate the state cache in the case of an
exception.
|
|
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaëtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
|
|
functionalization.
|
|
|
