partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lifts_vector.ma

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 a5310b63dce69cde3da9653a854b652b927ea979..d0cd506bc8f00549b6cc2aa7cb0177cc0876b149 100644 (file)
--- 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 ***************************************************)