Fixing a little bug in using the "where" clause for inductive types.

This was not working when the inductive type had implicit parameters.

This could still be improved. E.g. the following still does not work:

Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.

But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).

1 files changed, 6 insertions, 0 deletions

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 511b60b4b..8c83b196e 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -116,3 +116,9 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
+(* Check "where" clause for inductive types with parameters *)
+
+Reserved Notation "x === y" (at level 50).
+Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
+ where "x === y" := (EQ x y).