diff options
| author | Hugo Herbelin | 2020-05-09 15:05:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-09 15:05:33 +0200 |
| commit | 56e2d2fe23bfe69f7c181e3786e8e95f1ee6151b (patch) | |
| tree | a90ea6b71c1aa506c43ead2b55bfb4ffaa1f0866 /test-suite | |
| parent | 3d20cedd6c7a38e712a6d94ecf52158fe6aa49db (diff) | |
| parent | 4c39126f0a0a97152f67a3a5e7c86db860f48e39 (diff) | |
Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple scopes for the same inductive)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_12159.out | 28 | ||||
| -rw-r--r-- | test-suite/output/bug_12159.v | 39 |
2 files changed, 67 insertions, 0 deletions
diff --git a/test-suite/output/bug_12159.out b/test-suite/output/bug_12159.out new file mode 100644 index 0000000000..7f47c47e32 --- /dev/null +++ b/test-suite/output/bug_12159.out @@ -0,0 +1,28 @@ +f 1%B + : unit +f 0 + : unit +1%B + : unit +0 + : unit +1%B + : unit +1 + : unit +1 + : unit +0 + : unit +1 + : unit +0%A + : unit +1 + : unit +0%A + : unit +0 + : unit +0 + : unit diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v new file mode 100644 index 0000000000..91d66f7f4c --- /dev/null +++ b/test-suite/output/bug_12159.v @@ -0,0 +1,39 @@ +Declare Scope A. +Declare Scope B. +Delimit Scope A with A. +Delimit Scope B with B. +Definition to_unit (v : Decimal.uint) : option unit + := match Nat.of_uint v with O => Some tt | _ => None end. +Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. +Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1. +Numeral Notation unit to_unit of_unit : A. +Numeral Notation unit to_unit of_unit' : B. +Definition f x : unit := x. +Check f tt. +Arguments f x%A. +Check f tt. +Check tt. +Open Scope A. +Check tt. +Close Scope A. +Check tt. +Open Scope B. +Check tt. +Undelimit Scope B. +Check tt. +Open Scope A. +Check tt. +Close Scope A. +Check tt. +Close Scope B. +Check tt. +Open Scope B. +Check tt. +Notation "1" := true. +Check tt. +Open Scope A. +Check tt. +Declare Scope C. +Notation "0" := false : C. +Open Scope C. +Check tt. (* gives 0 but should now be 0%A *) |