| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
|
| | | |\ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
No functional changes, only a minor copy on a deprecated output
option.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
No functional change, even if we could optimize `blanch_utf8_string` a
bit more by using `String.init`.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:
```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
(shorter name to refer to it in current context is M.foo)
```
My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This was not working when the inductive type had implicit parameters.
This could still be improved. E.g. the following still does not work:
Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.
But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
| | | | | |
|
| | | | | |
|
| | |/ / |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| | | | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Types were a bit difficult to read as they were mostly based on
anonymous products, this commit replaces them by named records and
refactors out some imperative code.
There is still quite a bit of room for improvement, but at least the
records provide a basis for more fine-grained understanding and
documentation.
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | | |
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- We fix the inconsistency of Structure and Record which according to
doc are the same.
- We improve the error message when not using { ... } for Record or Structure.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
This is only a quick fix, as hinted by Jason.
|
| | | | | |
|
| |\| | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#366: Univs: fix bug 5208
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Parameter was implemented the wrong way trying to separate the universes
of the telescope.
|
| |\| | | | |
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
| | | | |
| | | |
| | | |
| | | | |
#3339).
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Recalculating the metric all the time was proving costly (it was obvious
even on small queries).
|
| | | | |
| | | |
| | | |
| | | | |
Having more disctinc symbols incurs a penalty.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
This orders the results of search commands (such as `Search`,
`SearchAbout`, …) according to a "relevance" metric to minimise.
In this minimal version, the metric is the size of the displayed term.
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Note that this is still broken when loading files containing C-zar scripts.
|
| | | | | | |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Ralf Jung
Guillaume Melquiond
Matthieu Sozeau
Arnaud Spiwack
Cyprien Mangin