From c5f6ebc56b2275699a0ceeac18a53dd8370c172b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 27 Jul 2005 08:14:59 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index c7bf99899..cb450fd34 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -77,6 +77,15 @@ TODO fetch/decode/execute delle linee dello script? Una possibile alternativa e' avere alias "soft": se la disambiguazione fallisce gli alias soft vengono ripuliti e si riprova. + SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias + implicito; 2. gli alias vengono ricordati come nella soluzione originale + (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono + dimenticati (quali? tutti?) e si ritenta; se fallisce ancora si generano + istanze differenti e si ritenta; 4. ritentare anche senza e poi con + coercions? oppure ordinare preferendo la soluzione che non ha introdotto + coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono + gli alias nello script viene un paciugo, credo! in particolare quando + vengono usate n istanze - matitamake foo/a.ma non funziona; bisogna chiamarlo con matitamake /x/y/z/foo/a.ma - notazione -> Luca e Zack -- 2.39.2