| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
|
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
Commit auto-generated by running dev/tools/update-compat.py --release.
As per release doc this must be run at some point before branching
(not necessarily close to the branching date).
|
|
Reviewed-by: herbelin
Ack-by: jfehrle
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
this directory
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
add an overlay for coquelicot
remove functions from RList: In, Rlength, cons_Rlist, app_RList
because they are essentially the same as In, length, app, and map from List
(beware that the order of arguments changes for map, and the In function
contains reversed equalities).
adds deprecation warnings for Rlist and Rlength
adds deprecated notations for RList.cons and RList.nil
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
|
|
|
|
|
