| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| |
|
|
|
| |
Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
|
| |\ |
|
| |\ \ |
|
| | |/ |
|
| | |\ |
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).
The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.
What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We add a more convenient API to create identifiers from mutable
strings. We cannot solve the `String.copy` deprecation problem until
we enable `-safe-string`.
|
| | | |
| | |
| | |
| | |
| | | |
This part of state is critical. We refactor it and make it into a
record to ease handling.
|
| | |/
| |
| |
| | |
We instead save the current value.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | |
|
| |/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| | |
| |
| |
| | |
This is a better (more generic) fix to #5061 than my e8b9ee76.
|
| | |
| |
| |
| |
| |
| | |
Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
|
| |\| |
|
| | |\
| | |
| | |
| | | |
Was PR#337: Fix arguments
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
|
| | |\ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:
https://en.wikipedia.org/wiki/Lambda_lifting
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Objects registered through the callback functions were pushed on the libstack
before the ML-MODULE object itself, leading to anomalies when the corresponding
object was assuming that the ML module was properly defined in any other Coq
module requiring the Declare ML command.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This is a bit ad-hoc, but looks better for warnings since there is
a command-line flag accepting the same values, so comma will lead to
fewer parsing issues than space.
|
| |\ \ \ |
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | | |
Whether an option should be set or appended to is stored as a 2-value
flag next to the new content. This commit also cleans the code by
declaring a single object for each persistent option rather than three
different ones (one per locality).
|
| | |\ \
| | | |
| | | |
| | | |
| | | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| | | |/
| |/|
| | |
| | |
| | |
| | | |
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
| | |/ |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It
seems that the original motivation was to deactivate a warning when overriding
the default loadpath binding of the current directory, but in the end it made
it non-overridable.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
| | | |
|
| |\ \ |
|
| |\ \ \
| | |/
| |/| |
|
| | | | |
|
| | | | |
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Matej Kosik
Guillaume Melquiond
Hugo Herbelin
Enrico Tassi