update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_max.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
index 44c3539b9eb0035c26509880827f14df182de90e..cb902736e1de5bbc7c1c02d33a2a79d4fadc4fad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
@@ -39,7 +39,7 @@ qed.
 (*** max_SS *)
 lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
 #n1 #n2
-@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *)
+@trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *)
 <ntri_f_tri //
 qed.