X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_vector.ma;h=d0cd506bc8f00549b6cc2aa7cb0177cc0876b149;hp=a5310b63dce69cde3da9653a854b652b927ea979;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma
index a5310b63d..d0cd506bc 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma
@@ -29,7 +29,7 @@ interpretation "generic relocation (term vector)"
    'RLiftStar f T1s T2s = (liftsv f T1s T2s).
 
 interpretation "uniform relocation (term vector)"
-   'RLift i T1s T2s = (liftsv (uni i) T1s T2s).
+   'RLift i T1s T2s = (liftsv (pr_uni i) T1s T2s).
 
 (* Basic inversion lemmas ***************************************************)