diff options
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -38,6 +38,8 @@ Tactics without adding new ones. Preexisting tactic `constr_eq_nounivs` can still be used if you really want to ignore universe constraints. +- Tactics and tactic notations now understand the `deprecated` attribute. + Tools - Coq_makefile lets one override or extend the following variables from @@ -68,6 +70,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 |