completed test

[helm.git] / helm / matita / tests / unfold.ma

diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma
index 4af22f1b97c03796db9dc34dc34fd94099bc16b5..d63dd50d46d8a6a8027234ff691815f4a71c537b 100644 (file)
--- 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.