decompose now works without premises

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

diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma
index b1c17185d08dfabb33aff29c2576307ad7cb59fb..5def3ec470f664e0ac00c32e1d0c49a97b81d697 100644 (file)
--- a/matita/tests/fguidi.ma
+++ b/matita/tests/fguidi.ma
@@ -113,5 +113,5 @@ qed.
 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
 intros 1. elim x; clear H. clear x. 
 auto paramodulation.
-fwd H1 [H]. decompose H.
+fwd H1 [H]. decompose.
 *)