From 5c82bcd1f87cc893319f2553c81a73c69b13b54d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Aug 2014 18:02:11 +0200
Subject: Reorganisation of intropattern code - emphasizing the different kinds
 of patterns - factorizing code of the non-naming intro-patterns

Still some questions:

- Should -> and <- apply to hypotheses or not (currently they apply to
  hypotheses either when used in assert-style tactics or apply in, or
  when the term to rewrite is a variable, in which case "subst" is
  applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
  posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
  quantifications?
---
 dev/doc/changes.txt | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 036bf1d5e3..4ea33ddbea 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -87,6 +87,10 @@
 
 - API of Inductiveops made more uniform (see commit log or file itself).
 
+- API of intros_pattern style tactic changed; "s" is dropped in
+  "intros_pattern" and "intros_patterns" is not anymore behaving like
+  tactic "intros" on the empty list.
+
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
-- 
cgit v1.2.3