- partial commit of rt_transition ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index 4fcb38e316e15050d6ffe51f83813c9860d66ead..e4e11049c910bddca67adfac03ffe6d7a1ef0922 100644 (file)
--- 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 ≝