diff options
| author | Gaëtan Gilbert | 2020-01-18 14:46:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-22 14:50:15 +0100 |
| commit | 71aa415282a93a6e23af3b824f8531c58d2d66bd (patch) | |
| tree | dc33334717fd6717036c2f716115820878a75d12 | |
| parent | 2c71d636f80327500ea75c1c1ce59c554001a078 (diff) | |
Fix #11421 computation of Set+2
| -rw-r--r-- | dev/doc/critical-bugs | 15 | ||||
| -rw-r--r-- | doc/changelog/01-kernel/11422-Setplus2.rst | 4 | ||||
| -rw-r--r-- | kernel/univ.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_11421.v | 1 |
4 files changed, 21 insertions, 3 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 2d187f7bae..3260040248 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -158,7 +158,7 @@ Universes 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 released versions: V8.5-V8.10 impacted development branches: none impacted coqchk versions: immune fixed in: PR#10664 @@ -167,6 +167,19 @@ Universes GH issue number: none risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + component: algebraic universes + summary: Set+2 was incorrectly simplified to Set+1 + introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a) + impacted released versions: V8.10.0 V8.10.1 V8.10.2 + impacted coqchk versions: same + fixed in: PR#11422 + found by: Gilbert + exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration) + GH issue number: see PR + risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic + universes such that +2 increments do not appear), mild risk from plugins which manipulate + algebraic universes. + Primitive projections component: primitive projections, guard condition diff --git a/doc/changelog/01-kernel/11422-Setplus2.rst b/doc/changelog/01-kernel/11422-Setplus2.rst new file mode 100644 index 0000000000..cc174358cc --- /dev/null +++ b/doc/changelog/01-kernel/11422-Setplus2.rst @@ -0,0 +1,4 @@ +- **Fixed:** + The type of :g:`Set+1` would be computed to be itself, leading to a proof of False. + (`#11422 <https://github.com/coq/coq/pull/11422>`_, + by Gaëtan Gilbert). diff --git a/kernel/univ.ml b/kernel/univ.ml index 51440147ad..0712774576 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -345,8 +345,8 @@ struct (Level.is_prop u && not (Level.is_sprop v)) else false - let successor (u,n) = - if Level.is_small u then type1 + let successor (u,n as e) = + if is_small e then type1 else (u, n + 1) let addn k (u,n as x) = diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v new file mode 100644 index 0000000000..8ddf05c888 --- /dev/null +++ b/test-suite/bugs/closed/bug_11421.v @@ -0,0 +1 @@ +Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}. |