...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 7f5cb644f3f3871abb6ccb8f7af3da188d17896b..c29a9a031dc1a5f96115c3834cf0129d0e96688c 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -14,7 +14,19 @@ TODO
   - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire,
     giusto?
   - comportamento di tutte le tattiche nei confronti dei let-in
-  - tattica unfold su rel a let-in bound variables
+  - tattica unfold su rel a let-in bound variables: c'e' ancora un bug
+    aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto
+    del goal e non in quello del pattern. Pertanto invece di cercare di
+    fare unfolding di x viene fatto unfolding di altro.
+    Soluzione: la funzione ProofEngineHelpers.select deve tornare una
+    funzione per rilocare i termini nel contesto giusto.
+    Esempio:
+     theorem t: let uno \def S O in uno + uno = S uno \to uno=uno.
+      intros. unfold uno in H.
+    NOTA: questo bug e' legato a quello di parsing in presenza di tattiche
+    con pattern, visto che in tal caso e' l'intero parsing a dover essere
+    fatto in un contesto differente. Risolvendo quel bug si risolve
+    automaticamente anche questo.
   - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
     True.
   - parsing contestuale (tattiche replace, change e forse altre)

diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma
index 28ffcf3f2d7dba97aeec48b497ef9b7d030758ca..4af22f1b97c03796db9dc34dc34fd94099bc16b5 100644 (file)
--- a/helm/matita/tests/unfold.ma
+++ b/helm/matita/tests/unfold.ma
@@ -30,3 +30,8 @@ theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
  rewrite > lem.
  reflexivity.
 qed.
+
+(* This test needs to parse "uno" in the context of the hypothesis H,
+   not in the context of the goal. *)
+theorem t: let uno \def S O in uno + uno = S uno \to uno=uno.
+ intros. unfold uno in H.