From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 8 Sep 2005 09:42:30 +0000 (+0000)
Subject: completed test
X-Git-Tag: V_0_1_2_1~63
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=db0d3618d7ef673cf3e4892e7deb54984c811144;p=helm.git

completed test
---

diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma
index 4af22f1b9..d63dd50d4 100644
--- a/helm/matita/tests/unfold.ma
+++ b/helm/matita/tests/unfold.ma
@@ -35,3 +35,5 @@ qed.
    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.
+ reflexivity.
+qed.