| Age | Commit message (Collapse) | Author |
|---|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
Add headers to a few files which were missing them.
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
|
|
We remove a few aliases present in the lower layers
[`Genintern/Tactypes`] from `Tacexpr`.
IMHO this enlarges the API for no good purpose, and difficults
analysis.
|
|
We move the last 3 types to more adequate places.
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.
We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
|
|
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
|
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
|
|
Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.
This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.
In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module
I chose the second solution as it seems to me like the most sensible
choice.
cc: #6512.
|
|
|
|
We generalize the possible use of levels to raw and glob printers.
This is potentially useful for printing ltac expressions which are the
glob level.
|
|
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
|
|
|
|
|
|
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
|
|
This commit also fixes range selectors being incorrectly displayed.
|
|
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).
|
|
|
|
|
|
|
|
|
|
It seems there were 4 copies of the same function in the code base.
|
|
|
|
|
|
Now it is a private field, locations are optional.
|
|
|
|
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
|
|
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.
|
