From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 22 Aug 2005 08:43:01 +0000 (+0000)
Subject: Comment removed.
X-Git-Tag: working_equations_only~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f2e93e2751e2bce2518502933b7169f99f2dbeb;p=helm.git

Comment removed.
---

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index a665ca85d..19f527e8f 100644
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -46,7 +46,7 @@ intros. apply False_ind. cut (is_S O). auto paramodulation. elim H. exact I.
 qed.
 
 theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O).
-intros. auto. (* paramodulation non trova la prova *)
+intros. auto.
 qed.
 
 theorem eq_gen_S_S: \forall m,n. (S m) = (S n) \to m = n.