From fedc831df9626a31cd0d26ee6b9e022b67f90c2a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Feb 2017 14:34:44 +0100
Subject: 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).
---
 test-suite/success/Notations.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 511b60b4bb..8c83b196e4 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).
-- 
cgit v1.2.3