| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The point is to emphasize stronglier when we are talking about
contexts or about arguments.
|
| | |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
The number of effective parameters was used where the number of
declarations in the signature of parameters should have been used.
|
| | | | | | | |
|
| | | | | |/
| | | | |
| | | | |
| | | | |
| | | | | |
Call to nf_betaiota was done on one side of the comparison preventing
the same message to be repeated twice but not on the other side.
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
| |/ / / / |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| | | | |
|
| |/ / |
|
| |\ \
| | |
| | |
| | | |
top of the linking chain.
|
| |\ \ \
| | | |
| | | |
| | | | |
from location in file
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Inductive-keyworded record failing even on non-dependent goal)
|
| | |_|_|/ / /
|/| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
On Win32, Sys.readdir translates the file names to the charset of the
local "code page", which may be not compatible with utf8.
Warnings referring to these names can be generated. These warnings may
be sent to CoqIDE. To ensure a utf8 compliant communication, we escape
non-utf8 file names under win32.
In the CoqIDE/Coq communication, Glib.IO.read_chars expects an
utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in
conversion input".
This fixes bug #5715 (Hangul characters not recognized in file names)
but this does not solve the case of an operating system mounting a
file system with a different coding convention than the default one,
i.e. unicode using "Normalization Form Canonical Decomposition" in
UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux,
(non-normalized?) UTF-16 for NTFS on Windows.
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | | |
A trick in counting spaces in a format was making the empty notation
not behaving correctly.
|
| | |_|/ /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
| |\ \ \ |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | | |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 53a50875 and a bit more: it also makes the check
for possibly ignoring formatting spaces irrelevant, since the previous
commit makes that curly brackets are not any more dropped for
printing.
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
| | |_|/
|/| |
| | |
| | | |
(from module List).
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|_|/
|/| | |
| | | |
| | | | |
Use the functional interface understand_tcc instead.
|
| | |_|/
|/| |
| | |
| | | |
This was already the case, but the API was not exposing this.
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
y , z".
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| |_|_|/ /
|/| | | | |
|
| | | | | | |
|
| | | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| | | | |
| | | |
| | | |
| | | | |
This was an easy to prove property that I somehow overlooked.
|
| |/ / /
| | |
| | |
| | |
| | | |
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
|
Hugo Herbelin
Maxime Dénès
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Matthieu Sozeau
Guillaume Melquiond
Pierre-Marie Pédrot
Paul Steckler
Amin Timany
Matej Košík