diff options
Diffstat (limited to 'test-suite/output')
| -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 *) |