1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v
new file mode 100644
index 00000000..c5bf3289
--- /dev/null
+++ b/test-suite/bugs/closed/4865.v
@@ -0,0 +1,52 @@
+(* Check discharge of arguments scopes + other checks *)
+
+(* This is bug #4865 *)
+
+Notation "<T>" := true : bool_scope.
+Section A.
+  Check negb <T>.
+  Global Arguments negb : clear scopes.
+  Fail Check negb <T>.
+End A.
+
+(* Check that no scope is re-computed *)
+Fail Check negb <T>.
+
+(* Another test about arguments scopes in sections *)
+
+Notation "0" := true.
+Section B.
+  Variable x : nat.
+  Let T := nat -> nat.
+  Definition f y : T := fun z => x + y + z.
+  Fail Check f 1 0.   (* 0 in nat, 0 in bool *)
+  Fail Check f 0 0.   (* 0 in nat, 0 in bool *)
+  Check f 0 1.        (* 0 and 1 in nat *)
+  Global Arguments f _%nat_scope _%nat_scope.
+  Check f 0 0.        (* both 0 in nat *)
+End B.
+
+(* Check that only the scope for the extra product on x is re-computed *)
+Check f 0 0 0.   (* All 0 in nat *)
+
+Section C.
+  Variable x : nat.
+  Let T := nat -> nat.
+  Definition g y : T := fun z => x + y + z.
+  Global Arguments g : clear scopes.
+  Check g 1.          (* 1 in nat *)
+End C.
+
+(* Check that only the scope for the extra product on x is re-computed *)
+Check g 0.            (* 0 in nat *)
+Fail Check g 0 1 0. (* 2nd 0 in bool *)
+Fail Check g 0 0 1. (* 2nd 0 in bool *)
+
+(* Another test on arguments scopes: checking scope for expanding arities *)
+(* Not sure this is very useful, but why not *)
+                  
+Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end.
+Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n  end.
+Notation "0" := true.
+Arguments Scope lam [nat_scope nat_scope].
+Check (lam 1 0).