From dfa99b152114271cf9fac4cab9d8663ac6ec078c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 May 2018 14:57:00 +0200 Subject: Fixes part 1 of #7462 (only-printing not to override existing interp rule). --- test-suite/bugs/closed/7462.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/7462.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v new file mode 100644 index 000000000..37af64caa --- /dev/null +++ b/test-suite/bugs/closed/7462.v @@ -0,0 +1,6 @@ +(* Adding an only-printing notation should not override existing + interpretations for the same notation. *) + +Notation "$ x" := (@id nat x) (only parsing, at level 0). +Notation "$ x" := (@id bool x) (only printing, at level 0). +Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *) -- cgit v1.2.3