Removing "intro" from the tactic AST.

Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.

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