From 2badc68c73958cc9bafb6d2f05c40546786f5da2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Jun 2005 10:51:09 +0000 Subject: [PATCH] fix --- helm/matita/matita.txt | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index d4365d1cc..4077a173c 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,7 +2,6 @@ (**********************************************************************) TODO -- uri_of_term and term_of_uri: cambiare il tipo per far tornare delle uri!!! - eta_expand non usata da nessuno? - eliminare eta_fix? (aspettare notazione da Zack e Luca) - bug di ferruccio: fare un refresh dei nomi dopo l'applicazione @@ -11,8 +10,6 @@ TODO esso un nome viene usato in maniera ambigua. Esempio: \lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh \lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh -- non eseguire comandi quando lo stato e' diverso da No_proof -- fare tornare a matitac -1 quando lo stato finale e' diverso da No_proof - a volte genera termini con variabili legate da piu' binder Capita quando un tipo dall'environment (e.g. \lambda x.T) viene inserito in un contesto (e.g. x:nat) dove le variabili @@ -26,6 +23,11 @@ TODO - tattica clear ? -> Gares DONE +- fare tornare a matitac -1 quando lo stato finale e' + diverso da No_proof, non eseguire comandi quando lo + stato e' diverso da No_proof -> CSC +- uri_of_term and term_of_uri: cambiare il tipo per far + tornare delle uri!!! -> CSC - intro = intros 1 -> Gares - timetravel (urimanager) -> Gares - implementare macro in matitaScript.ml -> Gares -- 2.39.2