diff options
| author | Maxime Dénès | 2019-09-26 10:59:39 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-26 10:59:39 +0200 |
| commit | 884b413e91d293a6b2009da11f2996db0654e40f (patch) | |
| tree | eb9ca92acdea668507f31659a5609f5570ea5be2 /dev | |
| parent | 59079a232d2157c0c4bea4cb1a3cd68c9410e880 (diff) | |
| parent | 6adc6e9484fde99ae943b31989f1454b6d079aaa (diff) | |
Merge PR #10664: Putting sections libstack inside the kernel
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
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 |