From cda674b91ec137bb4c995063888cc5059884ac8c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 3 Jul 2018 16:52:12 +0000 Subject: Document attributes. --- CHANGES | 2 ++ 1 file changed, 2 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 3ec53fad2..0a5ac56b7 100644 --- a/CHANGES +++ b/CHANGES @@ -58,6 +58,8 @@ Vernacular Commands - New Set Hint Variables/Constants Opaque/Transparent commands for setting globally the opacity flag of variables and constants in hint databases, overwritting the opacity set of the hint database. +- Added generic syntax for “attributes”, as in: + `#[local] Lemma foo : bar.` Coq binaries and process model -- cgit v1.2.3