diff options
Diffstat (limited to 'test-suite/modules/plik.v')
| -rw-r--r-- | test-suite/modules/plik.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v index 50bfd960..c2f0fe3c 100644 --- a/test-suite/modules/plik.v +++ b/test-suite/modules/plik.v @@ -1,3 +1,3 @@ Definition toto (x : Set) := x. -(* <Warning> : Grammar is replaced by Notation *)
\ No newline at end of file +(* <Warning> : Grammar is replaced by Notation *) |