aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 2 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 250386151..a474a84c5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -74,6 +74,8 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou
Arguments" et non plus selon la valeur qu'elle avait au moment de la
définition dans la section.
+- SearchPattern / SearchRewrite (contrib de Yves Bertot)
+
Tactiques
- Langage de tactique
@@ -90,8 +92,6 @@ Tactiques
en général plus son nom (sauf dans les cas "simples"). Rem : c'est une
source d'incompatibilité.
-- EAuto réussit parfois plus (source d'incompatibilité).
-
- Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement
- Plus de "Require Prolog" (intégré par défaut)