blob: 4c81095c68b9a7a715675244904f37ba999b09c0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* Until recently, the Notation.declare_numeral_notation wasn't synchronized
w.r.t. backtracking. This should be ok now.
This test is pretty artificial (we must declare Z_scope for this to work).
*)
Delimit Scope Z_scope with Z.
Open Scope Z_scope.
Check 0.
(* 0 : nat *)
Require BinInt.
Check 0.
(* 0 : BinNums.Z *)
Back 2.
Check 0.
(* Expected answer: 0 : nat *)
(* Used to fail with:
Error: Cannot interpret in Z_scope without requiring first module BinNums.
*)
|
