| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
information.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This ensures by construction that we never infer constraints outside
the variance model.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| | | | | |
|
| | | | | |
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | | |
We remove many individual calls to `msg_notice` in the print
vernacular dispatcher in favor of a single, top-level calls.
This is a minor refactoring but will help in handling `Print Foo` more uniformly.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ \ \ \ |
|
Maxime Dénès
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Vincent Laporte
Théo Zimmermann
Pierre-Marie Pédrot