- commit of the "substitution" component

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index b26b7e95b128caf163d94b776c92f82a106fcc7f..af0172fdb1e07f6913f4deb9715bf623e97e9522 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -36,11 +36,11 @@ inductive ldrop (s:bool): relation4 nat nat lenv lenv ≝
 interpretation
    "basic slicing (local environment) abstract"
    'RDrop s d e L1 L2 = (ldrop s d e L1 L2).
-
+(*
 interpretation
    "basic slicing (local environment) general"
    'RDrop d e L1 L2 = (ldrop true d e L1 L2).
-
+*)
 interpretation
    "basic slicing (local environment) lget"
    'RDrop e L1 L2 = (ldrop false O e L1 L2).