milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 1ff7afbb4c1945ff56bfca1781eca4a586177ce4..8096e849ba554d7164c90362c3897d1b395591fd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -17,7 +17,7 @@ include "ground/arith/pnat_iter.ma".
 (* ADDITION FOR POSITIVE INTEGERS *******************************************)
 
 definition pplus: pnat → pnat → pnat ≝
-           λp,q. psucc^q p.
+           λp,q. (psucc^q) p.
 
 interpretation
   "plus (positive integers)"