| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: jfehrle
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
|
|
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: 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>
|
|
Parameters)
Reviewed-by: Matafou
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
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.
|
|
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.
|
|
|
|
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
- 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
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
Reviewed-by: gares
|
|
This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)
It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.
|
|
This is the smallest possible change to clarify the text without making it
even more formal.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
|
|
|
|
- Mention Guillaume Claret among maintainers of the OPAM repository
(as suggested by Karl Palmskog).
- Update links to the documentation to avoid being outdated.
- Mention sections beyond the one on 8.11+beta1.
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
Fixes #10909: Set Default Proof Mode is not documented.
|
|
OCaml's string type
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
|
