| Age | Commit message (Collapse) | Author |
|---|
|
Interestingly, the documentation for Hint Resolve -> qualid was outdated.
It was claiming that any term would be accepted, but actually with this
particular syntax, only qualified names would be parsed already.
|
|
We restrict hints to be global references, so as to further simplify the
implementation. Allowing arbitrary terms makes it difficult or expensive
to handle properly some actions like universe contexts or hint equality.
Ultimately, the IsConstr constructor for hints should also be removed.
|
|
Reviewed-by: ejgallego
|
|
|
|
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
(inconsistencies in parsing/printing notations to partial applications)
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Reviewed-by: jfehrle
|
|
They were already deprecated in two major releases.
|
|
|
|
|
|
doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
Thanks
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
reserve parsing keywords
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
This is useful when we want to have finer control of the location of
files in the bootstrap process, for example when building using Dune.
Also, this makes options consistent with what `coqdep` already uses
for bootstrap.
The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust.
Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
|
|
Reviewed-by: pi8027
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Reviewed-by: anton-trunov
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
to control uniform parameters.
This replaces the attribute.
|
|
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
|
|
|
|
|
|
If it is for an internal non-terminal then:
- if for a subentry different from constr, it refers to the head of
the subentry
- if in constr, it is 200 by convention
If it is on the border of a rule, then:
- if it is in a subentry different from the entry it lives, it refers
to the head of the subentry (or 200 by convention if in constr)
- if it is in the same entry, the rule for associativity tells if a
SELF, a NEXT, or (if on the right) a LEVEL
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
"(tactic)" instead of "(tacn)"
Reviewed-by: Zimmi48
|
|
Parameters)
Reviewed-by: Matafou
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Ex: "(tactic)" instead of "(tacn)"
|
|
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:
- not used in the main build since a long time
- not tested
- not kept up to date with upstream
This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.
`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.
We also remove the residual `-slash` option.
|
|
missing them.
Reviewed-by: ejgallego
|
