1 files changed, 64 insertions, 0 deletions
diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
new file mode 100644
index 00000000..07986b0d
--- /dev/null
+++ b/test-suite/interactive/PrimNotation.v
@@ -0,0 +1,64 @@
+(* 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 let v := 0 in v : nat.
+(* let v := 0 in v : nat : nat *)
+Require BinInt.
+Check let v := 0 in v : BinNums.Z.
+(* let v := 0 in v : BinNums.Z : BinNums.Z *)
+Back 2.
+Check let v := 0 in v : nat.
+(* Expected answer: let v := 0 in v : nat : nat *)
+(* Used to fail with:
+Error: Cannot interpret in Z_scope without requiring first module BinNums.
+*)
+
+Local Set Universe Polymorphism.
+Delimit Scope punit_scope with punit.
+Delimit Scope pcunit_scope with pcunit.
+Delimit Scope int_scope with int.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope.
+Module A.
+  NonCumulative Inductive punit@{u} : Type@{u} := ptt.
+  Cumulative Inductive pcunit@{u} : Type@{u} := pctt.
+  Definition to_punit : Decimal.int -> option punit
+    := fun v => match v with 0%int => Some ptt | _ => None end.
+  Definition to_pcunit : Decimal.int -> option pcunit
+    := fun v => match v with 0%int => Some pctt | _ => None end.
+  Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Numeral Notation punit to_punit of_punit : punit_scope.
+  Check let v := 0%punit in v : punit.
+  Back 2.
+  Numeral Notation pcunit to_pcunit of_pcunit : punit_scope.
+  Check let v := 0%punit in v : pcunit.
+End A.
+Reset A.
+Local Unset Universe Polymorphism.
+Module A.
+  Inductive punit : Set := ptt.
+  Definition to_punit : Decimal.int -> option punit
+    := fun v => match v with 0%int => Some ptt | _ => None end.
+  Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Numeral Notation punit to_punit of_punit : punit_scope.
+  Check let v := 0%punit in v : punit.
+End A.
+Local Set Universe Polymorphism.
+Inductive punit@{u} : Type@{u} := ptt.
+Definition to_punit : Decimal.int -> option punit
+  := fun v => match v with 0%int => Some ptt | _ => None end.
+Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+Numeral Notation punit to_punit of_punit : punit_scope.
+Check let v := 0%punit in v : punit.
+Back 6. (* check backtracking of registering universe polymorphic constants *)
+Local Unset Universe Polymorphism.
+Inductive punit : Set := ptt.
+Definition to_punit : Decimal.int -> option punit
+  := fun v => match v with 0%int => Some ptt | _ => None end.
+Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+Numeral Notation punit to_punit of_punit : punit_scope.
+Check let v := 0%punit in v : punit.