X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fmr2_plus.ma;h=da3380da9cb9a740efc8aaa70478622242085f5b;hb=2002da6bcdbf12203a87a7d9630d738f67ede68c;hp=11ffaa40710a4b7d9b848e07601974aa139c37af;hpb=5102e7f780e83c7fef1d3826f81dfd37ee4028bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
index 11ffaa407..da3380da9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
@@ -16,7 +16,7 @@ include "ground_2/relocation/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
-let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with
+rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with
 [ nil2         ⇒ ◊
 | cons2 l m cs ⇒ {l + i, m} @ pluss cs i
 ].