diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 6 | ||||
| -rw-r--r-- | dev/doc/changes.md | 7 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | dev/doc/parsing.md | 6 | ||||
| -rw-r--r-- | dev/doc/shield-icon.png | bin | 2512 -> 8582 bytes |
5 files changed, 28 insertions, 3 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 8b0bf216e3..de3d5a3d15 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -175,6 +175,12 @@ local copy of Coq. For this purpose, Dune supports the `-p` option, so version of Coq libs, and use a "release" profile that for example enables stronger compiler optimizations. +## OPAM file generation + +`.opam` files are automatically generated by Dune from the package +descriptions in the `dune-project` file; see Dune's manual for more +details. + ## Stanzas `dune` files contain the so-called "stanzas", that may declare: diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6a6318f97a..5adeafaa38 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -30,6 +30,13 @@ Generic arguments: - Generic arguments: `wit_var` is deprecated, use `wit_hyp`. +Dumpglob: + +- The function `Dumpglob.pause` and `Dumpglob.continue` are replaced + by `Dumpglob.push_output` and `Dumpglob.pop_output`. This allows + plugins to temporarily change/pause the output of Dumpglob, and then + restore it to the original setting. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 066facd5db..37619833ac 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -312,6 +312,18 @@ Conversion machines risk: none without using -allow-sprop (off by default in 8.10.0), otherwise could be exploited by mistake +Side-effects + + component: side-effects + summary: polymorphic side-effects inside monomorphic definitions incorrectly handled as not inlined + introduced: ? + impacted released versions: at least from 8.6 to 8.12.0 + impacted coqchk versions: none (no side-effects in the checker) + found by: ppedrot + exploit: test-suite/bugs/closed/bug_13330.v + GH issue number: #13330 + risk: unlikely to be exploited by mistake, requires the use of unsafe tactics + Conflicts with axioms in library component: library of real numbers diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md index 4982e3e94d..4956b91d01 100644 --- a/dev/doc/parsing.md +++ b/dev/doc/parsing.md @@ -210,7 +210,7 @@ command. The first square bracket around a nonterminal definition is for groupi level definitions, which are separated with `|`, for example: ``` - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] | "4" LEFTA @@ -220,8 +220,8 @@ level definitions, which are separated with `|`, for example: Grammar extensions can specify what level they are modifying, for example: ``` - tactic_expr: LEVEL "1" [ RIGHTA - [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + ltac_expr: LEVEL "1" [ RIGHTA + [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } ] ]; ``` diff --git a/dev/doc/shield-icon.png b/dev/doc/shield-icon.png Binary files differindex 629e51a819..f4a5b6ff5e 100644 --- a/dev/doc/shield-icon.png +++ b/dev/doc/shield-icon.png |
