aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index ae055cb2f..7de101527 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,9 @@ Tactics
for which pattern can be omitted, as in regular pattern-matching).
- Tactic scopes in Ltac like constr: and ltac: now require parentheses around
their argument.
+- Every generic argument type declares a tactic scope of the form "name:(...)"
+ where name is the name of the argument. This generalizes the constr: and ltac:
+ instances.
Program