From 0c68df5ccdacb5d2ed50b533ad613723914dfee7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 24 Nov 2000 16:13:28 +0000
Subject: certains effets disparaissent a la sortie des sections, d'autres non
 (selon Summary.survive_section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 2503861513..a474a84c53 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)
-- 
cgit v1.2.3