X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_plus.ma;h=8fd6b5c47034a1cf6783ab55845b669dce8e9513;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=c5c6ade72cc63a23b7e66a659590000f3cc2e327;hpb=21de0d35017656c5a55528390b54b0b2ae395b44;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index c5c6ade72..8fd6b5c47 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -43,7 +43,7 @@ qed.
 
 lemma pplus_comm: commutative … pplus.
 #p elim p -p //
-qed-.
+qed-. (* * gets in the way with auto *)
 
 lemma pplus_assoc: associative … pplus.
 #p #q #r elim r -r //