Remove a few tactics from the Tacexpr AST.

Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 9c89cdb8e5..41d61ec459 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,9 @@ Tactics
 - 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.
+- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
+  a locally free identifier anymore. It must use e.g. the "fresh" primitive
+  instead (potential source of incompatibilities).
 
 Program