From 34e84eafe6615055071fbdc4aaee70c4c161a0fb Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 9 May 2019 13:39:25 +0000
Subject: [Attributes] Allow explicit value for two-valued attributes

Attributes that enable/disable a feature can have an explicit value
(default is enable when the attribute is present).

Three-valued boolean attributes do not support this:
what would `#[local(false)]` mean?
---
 test-suite/success/attribute_syntax.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index f4f59a3c16..4717759dec 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -20,6 +20,10 @@ Check ι _ ι.
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
 
-- 
cgit v1.2.3