X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;h=e4e11049c910bddca67adfac03ffe6d7a1ef0922;hb=c3904c007394068ed823575e3be3d73a9ad92cce;hp=4fcb38e316e15050d6ffe51f83813c9860d66ead;hpb=fb246e36bb7d2731016e686e2091f6a3704bb362;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index 4fcb38e31..e4e11049c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -34,7 +34,7 @@ inductive drops (c:bool): rtmap → relation lenv ≝
 interpretation "uniform slicing (local environment)"
    'RDropStar i L1 L2 = (drops true (uni i) L1 L2).
 
-interpretation "general slicing (local environment)"
+interpretation "generic slicing (local environment)"
    'RDropStar c f L1 L2 = (drops c f L1 L2).
 
 definition d_liftable1: relation2 lenv term → predicate bool ≝