diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Notations2.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 986908b7fc..dca0208fb0 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -185,3 +185,12 @@ Import A. Infix "+++" := Nat.add (at level 80). End M18. + +Module InheritanceArgumentScopes. + +Axiom p : forall (A:Type) (b:nat), A = A /\ b = b. +Check fun A n => p (A * A) (n * n). (* safety check *) +Notation q := @p. +Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *) + +End InheritanceArgumentScopes. |