From 3057d53b0bfbb3c15e9d9d6942b35dfef495fe24 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 30 Oct 2000 16:51:42 +0000
Subject: Ajouts pour les tactiques utilisateur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@783 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 TODO | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'TODO')

diff --git a/TODO b/TODO
index 0db457ab1c..3e348a1a69 100644
--- a/TODO
+++ b/TODO
@@ -9,15 +9,16 @@ Distribution:
 Environnement:
 
 - Faire fonctionner Search
+- Porter SearchIsos
 - Faire fonctionner Abstract
 - Faire fonctionner Reset
 - Décider s'il faut garder Transparent/Opaque et si oui, l'implanter
 - Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo) FAIT
 
-Tactiques
+Tactiques:
 
-- Choisir la précédence de Try/Orelse
 - Éviter si possible les '(
+- Réécrire AutoRewrite avec le langage de tactiques
 
 Noyau:
 
@@ -36,5 +37,6 @@ Doc:
 - une passe sur le chapitre extensions de syntaxe
 - une passe sur le chapitre Cases
 - documenter le langage de tactique et Field
+- revoir le chapitre sur les tactiques utilisateur
 - clarifier la sémantique de Decompose (i.e. travaille pas sous les ->)
-- faut-il mieux spécifier la sémantique de Simpl (??)
\ No newline at end of file
+- faut-il mieux spécifier la sémantique de Simpl (??)
-- 
cgit v1.2.3