diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-30 16:51:42 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-30 16:51:42 +0000 |
| commit | 3057d53b0bfbb3c15e9d9d6942b35dfef495fe24 (patch) | |
| tree | 6992a33f745c02098f4b6e10b4e93b32228b3c07 /TODO | |
| parent | d970f1a233053149ca4576b26df77f884b5c0d6f (diff) | |
Ajouts pour les tactiques utilisateur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'TODO')
| -rw-r--r-- | TODO | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -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 (??) |