diff options
| author | Pierre-Marie Pédrot | 2019-09-02 09:17:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 6adc6e9484fde99ae943b31989f1454b6d079aaa (patch) | |
| tree | 9a8f6e90dddfce49c48b2a9be857e592f6354c27 /dev | |
| parent | df563b34440f6ea14356843b7b1c402a99266910 (diff) | |
Adding documentation for the move of sections data to kernel.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/critical-bugs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index d00c8cb11a..78d7061259 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -129,6 +129,18 @@ Universes GH issue number: #9294 risk: moderate risk to be activated by chance + component: universe polymorphism, asynchronous proofs + summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section + introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one + impacted released: V8.5-V8.10 + impacted development branches: none + impacted coqchk versions: immune + fixed in: PR#10664 + found by: Pédrot + exploit: no test + GH issue number: none + risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + Primitive projections component: primitive projections, guard condition |